## Stream: maths

### Topic: FTC progress report

#### Yury G. Kudryashov (Jul 31 2020 at 01:04):

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.

#3640 has FTC-1

#### Yury G. Kudryashov (Jul 31 2020 at 06:20):

@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 (Jul 31 2020 at 11:45):

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

Last updated: May 10 2021 at 07:15 UTC