FTC progress report

Stream: maths

[Yury G. Kudryashov]

Here is a version of FTC I have now:

lemma continuous_at.integral_sub_linear_is_o_ae
  [topological_space α] [opens_measurable_space α]
  [normed_group E] [normed_space ℝ E] [second_countable_topology E] [complete_space E]
  [measurable_space E] [borel_space E]
  {μ : measure α} [locally_finite_measure μ] {a : α}
  {f : α → E} (ha : continuous_at f a) (hfm : measurable f) :
  is_o (λ s, ∫ x in s, f x ∂μ - (μ s).to_real • f a) (λ s, (μ s).to_real) ((𝓝 a).lift' powerset) :=

Now I just need to apply this to s = Ioc a x.

[Yury G. Kudryashov]

#3640 has FTC-1

[Yury G. Kudryashov]

@Anatole Dedecker I introduce typeclass filter.is_interval_generated. For filters on \R it is equivalent to "a filter has a basis which consists of connected sets". It can be useful as a way to speak about different filters in l'Hopital's rule (not sure).

[Anatole Dedecker]

Oooooh this may be useful indeed ! I need some time to think about it, but this is really interesting