English
Under IsAddHaarMeasure μ, f.normed μ(x) ≤ μ.real(closedBall(c,rOut)) divides by pow of K; i.e., f.normed μ(x) ≤ K^{finrank}/μ.real(closedBall(c,rOut)).
Русский
При IsAddHaarMeasure μ верно: f.normed μ(x) ≤ K^{финrank} / μ.real(closedBall(c,rOut)).
LaTeX
$$$ f.normed(\mu)(x) \le \dfrac{K^{\mathrm{finrank}\,\mathbb{R} E}}{\mu.real(\mathrm{closedBall}(c,f.rOut))} $$$
Lean4
theorem normed_le_div_measure_closedBall_rOut [IsAddHaarMeasure μ] (K : ℝ) (h : f.rOut ≤ K * f.rIn) (x : E) :
f.normed μ x ≤ K ^ finrank ℝ E / μ.real (closedBall c f.rOut) :=
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)
have : f x / ∫ y, f y ∂μ ≤ 1 / ∫ y, f y ∂μ := by
gcongr
· exact f.integral_pos.le
· exact f.le_one
apply this.trans
rw [div_le_div_iff₀ f.integral_pos, one_mul, ← div_le_iff₀' (pow_pos K_pos _)]
· exact f.measure_closedBall_div_le_integral μ K h
· exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rOut_pos).ne' measure_closedBall_lt_top.ne
