Zulip Chat Archive

Stream: maths

Topic: FTC progress report


view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 31 2020 at 06:17):

#3640 has FTC-1

view this post on Zulip 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).

view this post on Zulip 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