English
Assume (μ IsAddHaar) and a positive K with rOut ≤ K rIn. Then f.normed μ(x) ≤ K^{finrank} / μ.real(closedBall(c,rOut)) for all x.
Русский
При μ — мера Хаара и 0 < K с rOut ≤ K rIn верно: f.normed μ(x) ≤ K^{финорд} / μ.real(closedBall(c,rOut)) для всех x.
LaTeX
$$$ f.normed(\mu)(x) \le \dfrac{K^{\mathrm{finrank}\,\mathbb{R} E}}{\mu.real(\mathrm{closedBall}(c,f.rOut))} $$$
Lean4
theorem measure_closedBall_div_le_integral [IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) :
μ.real (closedBall c f.rOut) / K ^ finrank ℝ E ≤ ∫ x, f x ∂μ :=
by
have K_pos : 0 < K := by simpa [f.rIn_pos, not_lt.2 f.rIn_pos.le] using mul_pos_iff.1 (f.rOut_pos.trans_le h)
apply le_trans _ (f.measure_closedBall_le_integral μ)
rw [div_le_iff₀ (pow_pos K_pos _), addHaar_real_closedBall' _ _ f.rIn_pos.le,
addHaar_real_closedBall' _ _ f.rOut_pos.le, mul_assoc, mul_comm _ (K ^ _), ← mul_assoc, ← mul_pow, mul_comm _ K]
gcongr
exact f.rOut_pos.le
