English
If f has integral y and f and g are ae-equal on the box, then g has the same integral as f.
Русский
Если f имеет интеграл y и f совпадает ae почти всюду с g на коробке, то g имеет тот же интеграл, что и f.
LaTeX
$$$$\text{HasIntegral } I l f = y \quad\&\quad f =^\ae_{\mu|_I} g \Rightarrow \text{HasIntegral } I l g = y.$$$$
Lean4
/-- If `f` is a.e. equal to zero on a rectangular box, then it has McShane integral zero on this
box. -/
theorem of_aeEq_zero {l : IntegrationParams} {I : Box ι} {f : (ι → ℝ) → E} {μ : Measure (ι → ℝ)}
[IsLocallyFiniteMeasure μ] (hf : f =ᵐ[μ.restrict I] 0) (hl : l.bRiemann = false) :
HasIntegral.{u, v, v} I l f μ.toBoxAdditive.toSMul 0 := by
/- Each set `{x | n < ‖f x‖ ≤ n + 1}`, `n : ℕ`, has measure zero. We cover it by an open set of
measure less than `ε / 2 ^ n / (n + 1)`. Then the norm of the integral sum is less than `ε`. -/
refine hasIntegral_iff.2 fun ε ε0 => ?_
lift ε to ℝ≥0 using ε0.lt.le; rw [gt_iff_lt, NNReal.coe_pos] at ε0
rcases NNReal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩
haveI := Fact.mk (I.measure_coe_lt_top μ)
change μ.restrict I {x | f x ≠ 0} = 0 at hf
set N : (ι → ℝ) → ℕ := fun x => ⌈‖f x‖⌉₊
have N0 : ∀ {x}, N x = 0 ↔ f x = 0 := by simp [N]
have : ∀ n, ∃ U, N ⁻¹' { n } ⊆ U ∧ IsOpen U ∧ μ.restrict I U < δ n / n := fun n ↦
by
refine (N ⁻¹' { n }).exists_isOpen_lt_of_lt _ ?_
rcases n with - | n
· simp [ENNReal.div_zero (ENNReal.coe_pos.2 (δ0 _)).ne']
· refine (measure_mono_null ?_ hf).le.trans_lt ?_
· exact fun x hxN hxf => n.succ_ne_zero ((Eq.symm hxN).trans <| N0.2 hxf)
· simp [(δ0 _).ne']
choose U hNU hUo hμU using this
have : ∀ x, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ U (N x) := fun x =>
by
obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 ((hUo _).mem_nhds (hNU _ rfl))
exact ⟨⟨r, hr₀⟩, hr⟩
choose r hrU using this
refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ _ => ?_⟩
rw [dist_eq_norm, sub_zero, ← integralSum_fiberwise fun J => N (π.tag J)]
grw [← hcε, ← sum_le_hasSum _ (fun n _ => (δ n).2) (NNReal.hasSum_coe.2 hδc)]
apply norm_sum_le_of_le
rintro n -
dsimp [integralSum]
have : ∀ J ∈ π.filter fun J => N (π.tag J) = n, ‖μ.real ↑J • f (π.tag J)‖ ≤ μ.real J * n := fun J hJ ↦
by
rw [TaggedPrepartition.mem_filter] at hJ
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
gcongr
exact hJ.2 ▸ Nat.le_ceil _
refine (norm_sum_le_of_le _ this).trans ?_; clear this
rw [← sum_mul, ← Prepartition.measure_iUnion_toReal]
let m := μ (π.filter fun J => N (π.tag J) = n).iUnion
change m.toReal * ↑n ≤ ↑(δ n)
have : m < δ n / n := by
simp only [Measure.restrict_apply (hUo _).measurableSet] at hμU
refine (measure_mono ?_).trans_lt (hμU _)
simp only [Set.subset_def, TaggedPrepartition.mem_iUnion, TaggedPrepartition.mem_filter]
rintro x ⟨J, ⟨hJ, rfl⟩, hx⟩
exact ⟨hrU _ (hπ.1 _ hJ (Box.coe_subset_Icc hx)), π.le_of_mem' J hJ hx⟩
clear_value m
lift m to ℝ≥0 using ne_top_of_lt this
rw [ENNReal.coe_toReal, ← NNReal.coe_natCast, ← NNReal.coe_mul, NNReal.coe_le_coe, ← ENNReal.coe_le_coe,
ENNReal.coe_mul, ENNReal.coe_natCast, mul_comm]
exact (mul_le_mul_left' this.le _).trans ENNReal.mul_div_le
