Lean4
/-- The indicator function of a measurable set is McShane integrable with respect to any
locally-finite measure. -/
theorem hasIntegralIndicatorConst (l : IntegrationParams) (hl : l.bRiemann = false) {s : Set (ι → ℝ)}
(hs : MeasurableSet s) (I : Box ι) (y : E) (μ : Measure (ι → ℝ)) [IsLocallyFiniteMeasure μ] :
HasIntegral.{u, v, v} I l (s.indicator fun _ => y) μ.toBoxAdditive.toSMul (μ.real (s ∩ I) • y) :=
by
refine HasIntegral.of_mul ‖y‖ fun ε ε0 => ?_
lift ε to ℝ≥0 using ε0.le; rw [NNReal.coe_pos] at ε0
have A : μ (s ∩ Box.Icc I) ≠ ∞ := ((measure_mono Set.inter_subset_right).trans_lt (I.measure_Icc_lt_top μ)).ne
have B : μ (s ∩ I) ≠ ∞ := ((measure_mono Set.inter_subset_right).trans_lt (I.measure_coe_lt_top μ)).ne
obtain ⟨F, hFs, hFc, hμF⟩ : ∃ F, F ⊆ s ∩ Box.Icc I ∧ IsClosed F ∧ μ ((s ∩ Box.Icc I) \ F) < ε :=
(hs.inter I.measurableSet_Icc).exists_isClosed_diff_lt A (ENNReal.coe_pos.2 ε0).ne'
obtain ⟨U, hsU, hUo, hUt, hμU⟩ : ∃ U, s ∩ Box.Icc I ⊆ U ∧ IsOpen U ∧ μ U < ∞ ∧ μ (U \ (s ∩ Box.Icc I)) < ε :=
(hs.inter I.measurableSet_Icc).exists_isOpen_diff_lt A (ENNReal.coe_pos.2 ε0).ne'
have : ∀ x ∈ s ∩ Box.Icc I, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ U := fun x hx =>
by
rcases nhds_basis_closedBall.mem_iff.1 (hUo.mem_nhds <| hsU hx) with ⟨r, hr₀, hr⟩
exact ⟨⟨r, hr₀⟩, hr⟩
choose! rs hrsU using this
have : ∀ x ∈ Box.Icc I \ s, ∃ r : Ioi (0 : ℝ), closedBall x r ⊆ Fᶜ := fun x hx =>
by
obtain ⟨r, hr₀, hr⟩ := nhds_basis_closedBall.mem_iff.1 (hFc.isOpen_compl.mem_nhds fun hx' => hx.2 (hFs hx').1)
exact ⟨⟨r, hr₀⟩, hr⟩
choose! rs' hrs'F using this
classical
set r : (ι → ℝ) → Ioi (0 : ℝ) := s.piecewise rs rs'
refine ⟨fun _ => r, fun c => l.rCond_of_bRiemann_eq_false hl, fun c π hπ hπp => ?_⟩;
rw [mul_comm]
/- Then the union of boxes `J ∈ π` such that `π.tag ∈ s` includes `F` and is included by `U`,
hence its measure is `ε`-close to the measure of `s`. -/
dsimp [integralSum]
simp only [dist_eq_norm, ← indicator_const_smul_apply, sum_indicator_eq_sum_filter, ← sum_smul, ← sub_smul, norm_smul,
Real.norm_eq_abs, ← Prepartition.filter_boxes, ← Prepartition.measure_iUnion_toReal]
gcongr
set t := (π.filter (π.tag · ∈ s)).iUnion
change abs (μ.real t - μ.real (s ∩ I)) ≤ ε
have htU : t ⊆ U ∩ I :=
by
simp only [t, TaggedPrepartition.iUnion_def, iUnion_subset_iff, TaggedPrepartition.mem_filter, and_imp]
refine fun J hJ hJs x hx => ⟨hrsU _ ⟨hJs, π.tag_mem_Icc J⟩ ?_, π.le_of_mem' J hJ hx⟩
simpa only [r, s.piecewise_eq_of_mem _ _ hJs] using hπ.1 J hJ (Box.coe_subset_Icc hx)
refine abs_sub_le_iff.2 ⟨?_, ?_⟩
· refine (ENNReal.le_toReal_sub B).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
refine (tsub_le_tsub (measure_mono htU) le_rfl).trans (le_measure_diff.trans ?_)
refine (measure_mono fun x hx => ?_).trans hμU.le
exact ⟨hx.1.1, fun hx' => hx.2 ⟨hx'.1, hx.1.2⟩⟩
· have hμt : μ t ≠ ∞ := ((measure_mono (htU.trans inter_subset_left)).trans_lt hUt).ne
refine (ENNReal.le_toReal_sub hμt).trans (ENNReal.toReal_le_coe_of_le_coe ?_)
refine le_measure_diff.trans ((measure_mono ?_).trans hμF.le)
rintro x ⟨⟨hxs, hxI⟩, hxt⟩
refine ⟨⟨hxs, Box.coe_subset_Icc hxI⟩, fun hxF => hxt ?_⟩
simp only [t, TaggedPrepartition.iUnion_def, TaggedPrepartition.mem_filter, Set.mem_iUnion]
rcases hπp x hxI with ⟨J, hJπ, hxJ⟩
refine ⟨J, ⟨hJπ, ?_⟩, hxJ⟩
contrapose hxF
refine hrs'F _ ⟨π.tag_mem_Icc J, hxF⟩ ?_
simpa only [r, s.piecewise_eq_of_notMem _ _ hxF] using hπ.1 J hJπ (Box.coe_subset_Icc hxJ)
