Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit fc75855

Browse files
sgouezelsgouezel
committed
feat(measure_theory/*): refactor integral to allow non second-countable target space (#12942)
Currently, the Bochner integral in mathlib only allows second-countable target spaces. This is an issue, since many constructions in spectral theory require integrals, and spaces of operators are typically not second-countable. The most general definition of the Bochner integral requires functions that may take values in non second-countable spaces, but which are still pointwise limits of a sequence of simple functions (so-called strongly measurable functions) -- equivalently, they are measurable and with second-countable range. This PR refactors the Bochner integral, working with strongly measurable functions (or rather, almost everywhere strongly measurable functions, i.e., functions which coincide almost everywhere with a strongly measurable function). There are some prerequisistes (topological facts, and a good enough theory of almost everywhere strongly measurable functions) that have been PRed separately, but the remaining part of the change has to be done in one PR, as once one changes the basic definition of the integral one has to change all the files that depend on it. Once the change is done, in many files the fix is just to remove `[measurable_space E] [borel_space E] [second_countable_topology E]` to make the linter happy, and see that everything still compiles. (Well, sometimes it is also much more painful, of course :-). For end users using `integrable`, nothing has to be changed, but if you need to prove integrability by hand, instead of checking `ae_measurable` you need to check `ae_strongly_measurable`. In second-countable spaces, the two of them are equivalent (and you can use `ae_strongly_measurable.ae_measurable` and `ae_measurable.ae_strongly_measurable` to go between the two of them). The main changes are the following: * change `ae_eq_fun` to base it on equivalence classes of ae strongly measurable functions * fix everything that depends on this definition, including lp_space, set_to_L1, the Bochner integral and conditional expectation * fix everything that depends on these, notably complex analysis (removing second-countability and measurability assumptions all over the place) * A notion that involves a measurable function taking values in a normed space should probably better be rephrased in terms of strongly_measurable or ae_strongly_measurable. So, change a few definitions like `measurable_at_filter` (to `strongly_measurable_at_filter`) or `martingale`.
1 parent d28a163 commit fc75855

55 files changed

Lines changed: 1888 additions & 1638 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎counterexamples/phillips.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -416,7 +416,8 @@ begin
416416
simp [integral_indicator hs] },
417417
{ change integrable (indicator s 1) μ,
418418
have : integrable (λ x, (1 : ℝ)) μ := integrable_const (1 : ℝ),
419-
apply this.mono' (measurable.indicator (@measurable_const _ _ _ _ (1 : ℝ)) hs).ae_measurable,
419+
apply this.mono'
420+
(measurable.indicator (@measurable_const _ _ _ _ (1 : ℝ)) hs).ae_strongly_measurable,
420421
apply filter.eventually_of_forall,
421422
exact norm_indicator_le_one _ }
422423
end

‎src/analysis/ODE/picard_lindelof.lean‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -190,13 +190,11 @@ begin
190190
exact this.preimage continuous_map.continuous_coe
191191
end
192192

193-
variables [measurable_space E] [borel_space E]
194-
195193
lemma interval_integrable_v_comp (t₁ t₂ : ℝ) :
196194
interval_integrable f.v_comp volume t₁ t₂ :=
197195
(f.continuous_v_comp).interval_integrable _ _
198196

199-
variables [second_countable_topology E] [complete_space E]
197+
variables [complete_space E]
200198

201199
/-- The Picard-Lindelöf operator. This is a contracting map on `picard_lindelof.fun_space v` such
202200
that the fixed point of this map is the solution of the corresponding ODE.
@@ -224,7 +222,8 @@ begin
224222
have : has_deriv_within_at (λ t : ℝ, ∫ τ in v.t₀..t, f.v_comp τ) (f.v_comp t)
225223
(Icc v.t_min v.t_max) t,
226224
from integral_has_deriv_within_at_right (f.interval_integrable_v_comp _ _)
227-
(f.continuous_v_comp.measurable_at_filter _ _) f.continuous_v_comp.continuous_within_at,
225+
(f.continuous_v_comp.strongly_measurable_at_filter _ _)
226+
f.continuous_v_comp.continuous_within_at,
228227
rw v_comp_apply_coe at this,
229228
refine this.congr_of_eventually_eq_of_mem _ t.coe_prop,
230229
filter_upwards [self_mem_nhds_within] with _ ht',
@@ -276,10 +275,9 @@ end
276275

277276
end fun_space
278277

279-
variables [second_countable_topology E] [complete_space E]
278+
variables [complete_space E]
280279

281280
section
282-
variables [measurable_space E] [borel_space E]
283281

284282
lemma exists_contracting_iterate :
285283
∃ (N : ℕ) K, contracting_with K ((fun_space.next : v.fun_space → v.fun_space)^[N]) :=
@@ -302,7 +300,6 @@ lemma exists_solution :
302300
∃ f : ℝ → E, f v.t₀ = v.x₀ ∧ ∀ t ∈ Icc v.t_min v.t_max,
303301
has_deriv_within_at f (v t (f t)) (Icc v.t_min v.t_max) t :=
304302
begin
305-
borelize E,
306303
rcases v.exists_fixed with ⟨f, hf⟩,
307304
refine ⟨f ∘ v.proj, _, λ t ht, _⟩,
308305
{ simp only [(∘), proj_coe, f.map_t₀] },
@@ -315,7 +312,7 @@ end picard_lindelof
315312

316313
/-- Picard-Lindelöf (Cauchy-Lipschitz) theorem. -/
317314
lemma exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous
318-
[complete_space E] [second_countable_topology E]
315+
[complete_space E]
319316
{v : ℝ → E → E} {t_min t₀ t_max : ℝ} (ht₀ : t₀ ∈ Icc t_min t_max)
320317
(x₀ : E) {C R : ℝ} (hR : 0 ≤ R) {L : ℝ≥0}
321318
(Hlip : ∀ t ∈ Icc t_min t_max, lipschitz_on_with L (v t) (closed_ball x₀ R))

‎src/analysis/box_integral/integrability.lean‎

Lines changed: 15 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -192,44 +192,48 @@ open topological_space
192192

193193
/-- If `f : ℝⁿ → E` is Bochner integrable w.r.t. a locally finite measure `μ` on a rectangular box
194194
`I`, then it is McShane integrable on `I` with the same integral. -/
195-
lemma integrable_on.has_box_integral [second_countable_topology E] [measurable_space E]
196-
[borel_space E] [complete_space E] {f : (ι → ℝ) → E} {μ : measure (ι → ℝ)}
195+
lemma integrable_on.has_box_integral [complete_space E] {f : (ι → ℝ) → E} {μ : measure (ι → ℝ)}
197196
[is_locally_finite_measure μ] {I : box ι} (hf : integrable_on f I μ) (l : integration_params)
198197
(hl : l.bRiemann = ff) :
199198
has_integral.{u v v} I l f μ.to_box_additive.to_smul (∫ x in I, f x ∂ μ) :=
200199
begin
201-
/- First we replace an `ae_measurable` function by a measurable one. -/
202-
rcases hf.ae_measurable with ⟨g, hg, hfg⟩,
200+
borelize E,
201+
/- First we replace an `ae_strongly_measurable` function by a measurable one. -/
202+
rcases hf.ae_strongly_measurable with ⟨g, hg, hfg⟩,
203+
haveI : separable_space (range g ∪ {0} : set E) := hg.separable_space_range_union_singleton,
203204
rw integral_congr_ae hfg, have hgi : integrable_on g I μ := (integrable_congr hfg).1 hf,
204205
refine box_integral.has_integral.congr_ae _ hfg.symm hl,
205206
clear_dependent f,
206-
/- Now consider the sequence of simple functions `simple_func.approx_on g hg univ 0 trivial`
207+
/- Now consider the sequence of simple functions
208+
`simple_func.approx_on g hg.measurable (range g ∪ {0}) 0 (by simp)`
207209
approximating `g`. Recall some properties of this sequence. -/
208-
set f : ℕ → simple_func (ι → ℝ) E := simple_func.approx_on g hg univ 0 trivial,
209-
have hfi : ∀ n, integrable_on (f n) I μ, from simple_func.integrable_approx_on_univ hg hgi,
210+
set f : ℕ → simple_func (ι → ℝ) E :=
211+
simple_func.approx_on g hg.measurable (range g ∪ {0}) 0 (by simp),
212+
have hfi : ∀ n, integrable_on (f n) I μ,
213+
from simple_func.integrable_approx_on_range hg.measurable hgi,
210214
have hfi' := λ n, ((f n).has_box_integral μ I l hl).integrable,
211215
have hfgi : tendsto (λ n, (f n).integral (μ.restrict I)) at_top (𝓝 $ ∫ x in I, g x ∂μ),
212-
from tendsto_integral_approx_on_univ_of_measurable hg hgi,
216+
from tendsto_integral_approx_on_of_measurable_of_range_subset hg.measurable hgi _ subset.rfl,
213217
have hfg_mono : ∀ x {m n}, m ≤ n → ∥f n x - g x∥ ≤ ∥f m x - g x∥,
214218
{ intros x m n hmn,
215219
rw [← dist_eq_norm, ← dist_eq_norm, dist_nndist, dist_nndist, nnreal.coe_le_coe,
216220
← ennreal.coe_le_coe, ← edist_nndist, ← edist_nndist],
217-
exact simple_func.edist_approx_on_mono hg _ x hmn },
221+
exact simple_func.edist_approx_on_mono hg.measurable _ x hmn },
218222
/- Now consider `ε > 0`. We need to find `r` such that for any tagged partition subordinate
219223
to `r`, the integral sum is `(μ I + 1 + 1) * ε`-close to the Bochner integral. -/
220224
refine has_integral_of_mul ((μ I).to_real + 1 + 1) (λ ε ε0, _),
221225
lift ε to ℝ≥0 using ε0.le, rw nnreal.coe_pos at ε0, have ε0' := ennreal.coe_pos.2 ε0,
222226
/- Choose `N` such that the integral of `∥f N x - g x∥` is less than or equal to `ε`. -/
223227
obtain ⟨N₀, hN₀⟩ : ∃ N : ℕ, ∫ x in I, ∥f N x - g x∥ ∂μ ≤ ε,
224228
{ have : tendsto (λ n, ∫⁻ x in I, ∥f n x - g x∥₊ ∂μ) at_top (𝓝 0),
225-
from simple_func.tendsto_approx_on_univ_L1_nnnorm hg hgi,
229+
from simple_func.tendsto_approx_on_range_L1_nnnorm hg.measurable hgi,
226230
refine (this.eventually (ge_mem_nhds ε0')).exists.imp (λ N hN, _),
227231
exact integral_coe_le_of_lintegral_coe_le hN },
228232
/- For each `x`, we choose `Nx x ≥ N₀` such that `dist (f Nx x) (g x) ≤ ε`. -/
229233
have : ∀ x, ∃ N₁, N₀ ≤ N₁ ∧ dist (f N₁ x) (g x) ≤ ε,
230234
{ intro x,
231235
have : tendsto (λ n, f n x) at_top (𝓝 $ g x),
232-
from simple_func.tendsto_approx_on hg _ (subset_closure trivial),
236+
from simple_func.tendsto_approx_on hg.measurable _ (subset_closure (by simp)),
233237
exact ((eventually_ge_at_top N₀).and $ this $ closed_ball_mem_nhds _ ε0).exists },
234238
choose Nx hNx hNxε,
235239
/- We also choose a convergent series with `∑' i : ℕ, δ i < ε`. -/

‎src/analysis/calculus/fderiv_measurable.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel, Yury Kudryashov
55
-/
66
import analysis.calculus.deriv
77
import measure_theory.constructions.borel_space
8+
import measure_theory.function.strongly_measurable
89
import tactic.ring_exp
910

1011
/-!
@@ -407,6 +408,16 @@ variable {𝕜}
407408
[measurable_space F] [borel_space F] (f : 𝕜 → F) : measurable (deriv f) :=
408409
by simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1
409410

411+
lemma strongly_measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜]
412+
[second_countable_topology F] (f : 𝕜 → F) :
413+
strongly_measurable (deriv f) :=
414+
by { borelize F, exact (measurable_deriv f).strongly_measurable }
415+
410416
lemma ae_measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜] [measurable_space F]
411417
[borel_space F] (f : 𝕜 → F) (μ : measure 𝕜) : ae_measurable (deriv f) μ :=
412418
(measurable_deriv f).ae_measurable
419+
420+
lemma ae_strongly_measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜]
421+
[second_countable_topology F] (f : 𝕜 → F) (μ : measure 𝕜) :
422+
ae_strongly_measurable (deriv f) μ :=
423+
(strongly_measurable_deriv f).ae_strongly_measurable

‎src/analysis/calculus/parametric_integral.lean‎

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -58,9 +58,8 @@ open_locale topological_space filter
5858

5959
variables {α : Type*} [measurable_space α] {μ : measure α} {𝕜 : Type*} [is_R_or_C 𝕜]
6060
{E : Type*} [normed_group E] [normed_space ℝ E] [normed_space 𝕜 E]
61-
[complete_space E] [second_countable_topology E]
62-
[measurable_space E] [borel_space E]
63-
{H : Type*} [normed_group H] [normed_space 𝕜 H] [second_countable_topology $ H →L[𝕜] E]
61+
[complete_space E]
62+
{H : Type*} [normed_group H] [normed_space 𝕜 H]
6463

6564
/-- Differentiation under integral of `x ↦ ∫ F x a` at a given point `x₀`, assuming `F x₀` is
6665
integrable, `∥F x a - F x₀ a∥ ≤ bound a * ∥x - x₀∥` for `x` in a ball around `x₀` for ae `a` with
@@ -70,15 +69,14 @@ slightly less general but usually more useful version. -/
7069
lemma has_fderiv_at_integral_of_dominated_loc_of_lip' {F : H → α → E} {F' : α → (H →L[𝕜] E)}
7170
{x₀ : H} {bound : α → ℝ}
7271
{ε : ℝ} (ε_pos : 0 < ε)
73-
(hF_meas : ∀ x ∈ ball x₀ ε, ae_measurable (F x) μ)
72+
(hF_meas : ∀ x ∈ ball x₀ ε, ae_strongly_measurable (F x) μ)
7473
(hF_int : integrable (F x₀) μ)
75-
(hF'_meas : ae_measurable F' μ)
74+
(hF'_meas : ae_strongly_measurable F' μ)
7675
(h_lipsch : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ∥F x a - F x₀ a∥ ≤ bound a * ∥x - x₀∥)
7776
(bound_integrable : integrable (bound : α → ℝ) μ)
7877
(h_diff : ∀ᵐ a ∂μ, has_fderiv_at (λ x, F x a) (F' a) x₀) :
7978
integrable F' μ ∧ has_fderiv_at (λ x, ∫ a, F x a ∂μ) (∫ a, F' a ∂μ) x₀ :=
8079
begin
81-
letI : measurable_space 𝕜 := borel 𝕜, haveI : opens_measurable_space 𝕜 := ⟨le_rfl⟩,
8280
have x₀_in : x₀ ∈ ball x₀ ε := mem_ball_self ε_pos,
8381
have nneg : ∀ x, 0 ≤ ∥x - x₀∥⁻¹ := λ x, inv_nonneg.mpr (norm_nonneg _) ,
8482
set b : α → ℝ := λ a, |bound a|,
@@ -118,7 +116,7 @@ begin
118116
← show ∫ (a : α), ∥x₀ - x₀∥⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ = 0, by simp],
119117
apply tendsto_integral_filter_of_dominated_convergence,
120118
{ filter_upwards [h_ball] with _ x_in,
121-
apply ae_measurable.const_smul,
119+
apply ae_strongly_measurable.const_smul,
122120
exact ((hF_meas _ x_in).sub (hF_meas _ x₀_in)).sub (hF'_meas.apply_continuous_linear_map _) },
123121
{ apply mem_of_superset h_ball,
124122
intros x hx,
@@ -158,15 +156,15 @@ for `x` in a possibly smaller neighborhood of `x₀`. -/
158156
lemma has_fderiv_at_integral_of_dominated_loc_of_lip {F : H → α → E} {F' : α → (H →L[𝕜] E)} {x₀ : H}
159157
{bound : α → ℝ}
160158
{ε : ℝ} (ε_pos : 0 < ε)
161-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) μ)
159+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) μ)
162160
(hF_int : integrable (F x₀) μ)
163-
(hF'_meas : ae_measurable F' μ)
161+
(hF'_meas : ae_strongly_measurable F' μ)
164162
(h_lip : ∀ᵐ a ∂μ, lipschitz_on_with (real.nnabs $ bound a) (λ x, F x a) (ball x₀ ε))
165163
(bound_integrable : integrable (bound : α → ℝ) μ)
166164
(h_diff : ∀ᵐ a ∂μ, has_fderiv_at (λ x, F x a) (F' a) x₀) :
167165
integrable F' μ ∧ has_fderiv_at (λ x, ∫ a, F x a ∂μ) (∫ a, F' a ∂μ) x₀ :=
168166
begin
169-
obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ x ∈ ball x₀ δ, ae_measurable (F x) μ ∧ x ∈ ball x₀ ε,
167+
obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ x ∈ ball x₀ δ, ae_strongly_measurable (F x) μ ∧ x ∈ ball x₀ ε,
170168
from eventually_nhds_iff_ball.mp (hF_meas.and (ball_mem_nhds x₀ ε_pos)),
171169
choose hδ_meas hδε using hδ,
172170
replace h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ∥F x a - F x₀ a∥ ≤ |bound a| * ∥x - x₀∥,
@@ -182,9 +180,9 @@ and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`.
182180
lemma has_fderiv_at_integral_of_dominated_of_fderiv_le {F : H → α → E} {F' : H → α → (H →L[𝕜] E)}
183181
{x₀ : H} {bound : α → ℝ}
184182
{ε : ℝ} (ε_pos : 0 < ε)
185-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) μ)
183+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) μ)
186184
(hF_int : integrable (F x₀) μ)
187-
(hF'_meas : ae_measurable (F' x₀) μ)
185+
(hF'_meas : ae_strongly_measurable (F' x₀) μ)
188186
(h_bound : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ∥F' x a∥ ≤ bound a)
189187
(bound_integrable : integrable (bound : α → ℝ) μ)
190188
(h_diff : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, has_fderiv_at (λ x, F x a) (F' x a) x) :
@@ -211,19 +209,18 @@ assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball ar
211209
ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
212210
lemma has_deriv_at_integral_of_dominated_loc_of_lip {F : 𝕜 → α → E} {F' : α → E} {x₀ : 𝕜}
213211
{ε : ℝ} (ε_pos : 0 < ε)
214-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) μ)
212+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) μ)
215213
(hF_int : integrable (F x₀) μ)
216-
(hF'_meas : ae_measurable F' μ) {bound : α → ℝ}
214+
(hF'_meas : ae_strongly_measurable F' μ) {bound : α → ℝ}
217215
(h_lipsch : ∀ᵐ a ∂μ, lipschitz_on_with (real.nnabs $ bound a) (λ x, F x a) (ball x₀ ε))
218216
(bound_integrable : integrable (bound : α → ℝ) μ)
219217
(h_diff : ∀ᵐ a ∂μ, has_deriv_at (λ x, F x a) (F' a) x₀) :
220218
(integrable F' μ) ∧ has_deriv_at (λ x, ∫ a, F x a ∂μ) (∫ a, F' a ∂μ) x₀ :=
221219
begin
222-
letI : measurable_space 𝕜 := borel 𝕜, haveI : opens_measurable_space 𝕜 := ⟨le_rfl⟩,
223220
set L : E →L[𝕜] (𝕜 →L[𝕜] E) := (continuous_linear_map.smul_rightL 𝕜 𝕜 E 1),
224221
replace h_diff : ∀ᵐ a ∂μ, has_fderiv_at (λ x, F x a) (L (F' a)) x₀ :=
225222
h_diff.mono (λ x hx, hx.has_fderiv_at),
226-
have hm : ae_measurable (L ∘ F') μ := L.continuous.measurable.comp_ae_measurable hF'_meas,
223+
have hm : ae_strongly_measurable (L ∘ F') μ := L.continuous.comp_ae_strongly_measurable hF'_meas,
227224
cases has_fderiv_at_integral_of_dominated_loc_of_lip ε_pos hF_meas hF_int hm h_lipsch
228225
bound_integrable h_diff with hF'_int key,
229226
replace hF'_int : integrable F' μ,
@@ -244,9 +241,9 @@ end
244241
function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
245242
lemma has_deriv_at_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → α → E} {F' : 𝕜 → α → E} {x₀ : 𝕜}
246243
{ε : ℝ} (ε_pos : 0 < ε)
247-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) μ)
244+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) μ)
248245
(hF_int : integrable (F x₀) μ)
249-
(hF'_meas : ae_measurable (F' x₀) μ)
246+
(hF'_meas : ae_strongly_measurable (F' x₀) μ)
250247
{bound : α → ℝ}
251248
(h_bound : ∀ᵐ a ∂μ, ∀ x ∈ ball x₀ ε, ∥F' x a∥ ≤ bound a)
252249
(bound_integrable : integrable bound μ)

‎src/analysis/calculus/parametric_interval_integral.lean‎

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,8 @@ open_locale topological_space filter interval
1818

1919
variables {𝕜 : Type*} [is_R_or_C 𝕜] {μ : measure ℝ}
2020
{E : Type*} [normed_group E] [normed_space ℝ E] [normed_space 𝕜 E]
21-
[complete_space E] [second_countable_topology E]
22-
[measurable_space E] [borel_space E]
23-
{H : Type*} [normed_group H] [normed_space 𝕜 H] [second_countable_topology $ H →L[𝕜] E]
21+
[complete_space E]
22+
{H : Type*} [normed_group H] [normed_space 𝕜 H]
2423
{a b ε : ℝ} {bound : ℝ → ℝ}
2524

2625
namespace interval_integral
@@ -31,9 +30,9 @@ namespace interval_integral
3130
for `x` in a possibly smaller neighborhood of `x₀`. -/
3231
lemma has_fderiv_at_integral_of_dominated_loc_of_lip {F : H → ℝ → E} {F' : ℝ → (H →L[𝕜] E)} {x₀ : H}
3332
(ε_pos : 0 < ε)
34-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
33+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) (μ.restrict (Ι a b)))
3534
(hF_int : interval_integrable (F x₀) μ a b)
36-
(hF'_meas : ae_measurable F' (μ.restrict (Ι a b)))
35+
(hF'_meas : ae_strongly_measurable F' (μ.restrict (Ι a b)))
3736
(h_lip : ∀ᵐ t ∂μ, t ∈ Ι a b → lipschitz_on_with (real.nnabs $ bound t) (λ x, F x t) (ball x₀ ε))
3837
(bound_integrable : interval_integrable bound μ a b)
3938
(h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → has_fderiv_at (λ x, F x t) (F' t) x₀) :
@@ -53,9 +52,9 @@ derivative norm uniformly bounded by an integrable function (the ball radius is
5352
and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
5453
lemma has_fderiv_at_integral_of_dominated_of_fderiv_le {F : H → ℝ → E} {F' : H → ℝ → (H →L[𝕜] E)}
5554
{x₀ : H} (ε_pos : 0 < ε)
56-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
55+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) (μ.restrict (Ι a b)))
5756
(hF_int : interval_integrable (F x₀) μ a b)
58-
(hF'_meas : ae_measurable (F' x₀) (μ.restrict (Ι a b)))
57+
(hF'_meas : ae_strongly_measurable (F' x₀) (μ.restrict (Ι a b)))
5958
(h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ∥F' x t∥ ≤ bound t)
6059
(bound_integrable : interval_integrable bound μ a b)
6160
(h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, has_fderiv_at (λ x, F x t) (F' x t) x) :
@@ -73,9 +72,9 @@ assuming `F x₀` is integrable, `x ↦ F x a` is locally Lipschitz on a ball ar
7372
ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
7473
lemma has_deriv_at_integral_of_dominated_loc_of_lip {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜}
7574
(ε_pos : 0 < ε)
76-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
75+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) (μ.restrict (Ι a b)))
7776
(hF_int : interval_integrable (F x₀) μ a b)
78-
(hF'_meas : ae_measurable F' (μ.restrict (Ι a b)))
77+
(hF'_meas : ae_strongly_measurable F' (μ.restrict (Ι a b)))
7978
(h_lipsch : ∀ᵐ t ∂μ, t ∈ Ι a b →
8079
lipschitz_on_with (real.nnabs $ bound t) (λ x, F x t) (ball x₀ ε))
8180
(bound_integrable : interval_integrable (bound : ℝ → ℝ) μ a b)
@@ -96,9 +95,9 @@ assuming `F x₀` is integrable, `x ↦ F x a` is differentiable on an interval
9695
function, and `F x` is ae-measurable for `x` in a possibly smaller neighborhood of `x₀`. -/
9796
lemma has_deriv_at_integral_of_dominated_loc_of_deriv_le {F : 𝕜 → ℝ → E} {F' : 𝕜 → ℝ → E} {x₀ : 𝕜}
9897
(ε_pos : 0 < ε)
99-
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_measurable (F x) (μ.restrict (Ι a b)))
98+
(hF_meas : ∀ᶠ x in 𝓝 x₀, ae_strongly_measurable (F x) (μ.restrict (Ι a b)))
10099
(hF_int : interval_integrable (F x₀) μ a b)
101-
(hF'_meas : ae_measurable (F' x₀) (μ.restrict (Ι a b)))
100+
(hF'_meas : ae_strongly_measurable (F' x₀) (μ.restrict (Ι a b)))
102101
(h_bound : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ∥F' x t∥ ≤ bound t)
103102
(bound_integrable : interval_integrable bound μ a b)
104103
(h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, has_deriv_at (λ x, F x t) (F' x t) x) :

0 commit comments

Comments
 (0)