English
A Lipschitz-approximate derivative bounds the image measure by a factor controlled by the determinant, in Haar-measure spaces.
Русский
Приближённая по Липшицу производная ограничивает меру образа через детерминант, в пространствах с Haar-мерой.
LaTeX
$$$$ \forall A, \exists m>0: \text{if } f\text{ is close to } A, \ μ(f''s) \le m \cdot μ(s). $$$$
Lean4
/-- Let `f` be a function which is sufficiently close (in the Lipschitz sense) to a given linear
map `A`. Then it expands the volume of any set by at least `m` for any `m < det A`. -/
theorem mul_le_addHaar_image_of_lt_det (A : E →L[ℝ] E) {m : ℝ≥0} (hm : (m : ℝ≥0∞) < ENNReal.ofReal |A.det|) :
∀ᶠ δ in 𝓝[>] (0 : ℝ≥0), ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → (m : ℝ≥0∞) * μ s ≤ μ (f '' s) :=
by
apply nhdsWithin_le_nhds
rcases eq_or_lt_of_le (zero_le m) with (rfl | mpos)
· filter_upwards
simp only [forall_const, zero_mul, imp_true_iff, zero_le, ENNReal.coe_zero]
have hA : A.det ≠ 0 := by intro h; simp only [h, ENNReal.not_lt_zero, ENNReal.ofReal_zero, abs_zero] at hm
let B := A.toContinuousLinearEquivOfDetNeZero hA
have I : ENNReal.ofReal |(B.symm : E →L[ℝ] E).det| < (m⁻¹ : ℝ≥0) :=
by
simp only [ENNReal.ofReal, abs_inv, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm,
ENNReal.coe_lt_coe] at hm ⊢
exact NNReal.inv_lt_inv mpos.ne' hm
obtain ⟨δ₀, δ₀pos, hδ₀⟩ :
∃ δ : ℝ≥0,
0 < δ ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t :=
by
have :
∀ᶠ δ : ℝ≥0 in 𝓝[>] 0,
∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t :=
addHaar_image_le_mul_of_det_lt μ B.symm I
rcases (this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩
exact
⟨δ₀, h', h⟩
-- record smallness conditions for `δ` that will be needed to apply `hδ₀` below.
have L1 : ∀ᶠ δ in 𝓝 (0 : ℝ≥0), Subsingleton E ∨ δ < ‖(B.symm : E →L[ℝ] E)‖₊⁻¹ :=
by
by_cases h : Subsingleton E
· simp only [h, true_or, eventually_const]
simp only [h, false_or]
apply Iio_mem_nhds
simpa only [h, false_or, inv_pos] using B.subsingleton_or_nnnorm_symm_pos
have L2 : ∀ᶠ δ in 𝓝 (0 : ℝ≥0), ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀ :=
by
have :
Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
(𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) :=
by
rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
· simpa only [H, zero_mul] using tendsto_const_nhds
refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
simpa only [tsub_zero, inv_eq_zero, Ne] using H
simp only [mul_zero] at this
exact (tendsto_order.1 this).2 δ₀ δ₀pos
filter_upwards [L1, L2]
intro δ h1δ h2δ s f hf
have hf' : ApproximatesLinearOn f (B : E →L[ℝ] E) s δ := by convert hf
let F := hf'.toPartialEquiv h1δ
suffices H : μ (F.symm '' F.target) ≤ (m⁻¹ : ℝ≥0) * μ F.target
by
change (m : ℝ≥0∞) * μ F.source ≤ μ F.target
rwa [← F.symm_image_target_eq_source, mul_comm, ← ENNReal.le_div_iff_mul_le, div_eq_mul_inv, mul_comm, ←
ENNReal.coe_inv mpos.ne']
· apply Or.inl
simpa only [ENNReal.coe_eq_zero, Ne] using mpos.ne'
·
simp only [ENNReal.coe_ne_top, true_or, Ne, not_false_iff]
-- as `f⁻¹` is well approximated by `B⁻¹`, the conclusion follows from `hδ₀`
-- and our choice of `δ`.
exact hδ₀ _ _ ((hf'.to_inv h1δ).mono_num h2δ.le)
