Lean4
theorem addHaar_image_le_lintegral_abs_det_fderiv_aux1 (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) {ε : ℝ≥0} (εpos : 0 < ε) :
μ (f '' s) ≤ (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s := by
/- To bound `μ (f '' s)`, we cover `s` by sets where `f` is well-approximated by linear maps
`A n` (and where `f'` is almost everywhere close to `A n`), and then use that `f` expands the
measure of such a set by at most `(A n).det + ε`. -/
have :
∀ A : E →L[ℝ] E,
∃ δ : ℝ≥0,
0 < δ ∧
(∀ B : E →L[ℝ] E, ‖B - A‖ ≤ δ → |B.det - A.det| ≤ ε) ∧
∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ε) * μ t :=
by
intro A
let m : ℝ≥0 := Real.toNNReal |A.det| + ε
have I : ENNReal.ofReal |A.det| < m := by
simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]
rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δpos⟩
obtain ⟨δ', δ'pos, hδ'⟩ : ∃ (δ' : ℝ), 0 < δ' ∧ ∀ B, dist B A < δ' → dist B.det A.det < ↑ε :=
by
refine continuousAt_iff.1 ?_ ε εpos
exact ContinuousLinearMap.continuous_det.continuousAt
let δ'' : ℝ≥0 := ⟨δ' / 2, (half_pos δ'pos).le⟩
refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩
· intro B hB
rw [← Real.dist_eq]
apply (hδ' B _).le
rw [dist_eq_norm]
calc
‖B - A‖ ≤ (min δ δ'' : ℝ≥0) := hB
_ ≤ δ'' := by simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]
_ < δ' := half_lt_self δ'pos
· intro t g htg
exact h t g (htg.mono_num (min_le_left _ _))
choose δ hδ using this
obtain ⟨t, A, t_disj, t_meas, t_cover, ht, -⟩ :
∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
Pairwise (Disjoint on t) ∧
(∀ n : ℕ, MeasurableSet (t n)) ∧
(s ⊆ ⋃ n : ℕ, t n) ∧
(∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧ (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'
calc
μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
apply measure_mono
rw [← image_iUnion, ← inter_iUnion]
exact Set.image_mono (subset_inter Subset.rfl t_cover)
_ ≤ ∑' n, μ (f '' (s ∩ t n)) := (measure_iUnion_le _)
_ ≤ ∑' n, (ENNReal.ofReal |(A n).det| + ε) * μ (s ∩ t n) :=
by
apply ENNReal.tsum_le_tsum fun n => ?_
apply (hδ (A n)).2.2
exact ht n
_ = ∑' n, ∫⁻ _ in s ∩ t n, ENNReal.ofReal |(A n).det| + ε ∂μ := by
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
_ ≤ ∑' n, ∫⁻ x in s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ :=
by
apply ENNReal.tsum_le_tsum fun n => ?_
apply lintegral_mono_ae
filter_upwards [(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>
(hf' x hx.1).mono inter_subset_left]
intro x hx
have I : |(A n).det| ≤ |(f' x).det| + ε :=
calc
|(A n).det| = |(f' x).det - ((f' x).det - (A n).det)| := by congr 1; abel
_ ≤ |(f' x).det| + |(f' x).det - (A n).det| := (abs_sub _ _)
_ ≤ |(f' x).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ hx)
calc
ENNReal.ofReal |(A n).det| + ε ≤ ENNReal.ofReal (|(f' x).det| + ε) + ε := by gcongr
_ = ENNReal.ofReal |(f' x).det| + 2 * ε := by
simp only [ENNReal.ofReal_add, abs_nonneg, two_mul, add_assoc, NNReal.zero_le_coe, ENNReal.ofReal_coe_nnreal]
_ = ∫⁻ x in ⋃ n, s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ :=
by
have M : ∀ n : ℕ, MeasurableSet (s ∩ t n) := fun n => hs.inter (t_meas n)
rw [lintegral_iUnion M]
exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
_ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by
rw [← inter_iUnion, inter_eq_self_of_subset_left t_cover]
_ = (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s := by
simp only [lintegral_add_right' _ aemeasurable_const, setLIntegral_const]
