English
If a measure μ on a group G is invariant under taking inverses (i.e., μ is inv-invariant), then μ equals its inverse μ.inv.
Русский
Если мера μ на группе G незменяема при взятии обратной, то μ совпадает с μ.inv.
LaTeX
$$$ μ.inv = μ $$$
Lean4
/-- This lemma is weaker than `MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le`
as the latter provides `0 ≤ M` and does not require the measurability of `f`. -/
theorem integral_indicator_norm_ge_le (hf : MemLp f 1 μ) (hmeas : StronglyMeasurable f) {ε : ℝ} (hε : 0 < ε) :
∃ M : ℝ, (∫⁻ x, ‖{x | M ≤ ‖f x‖₊}.indicator f x‖₊ ∂μ) ≤ ENNReal.ofReal ε :=
by
have htendsto : ∀ᵐ x ∂μ, Tendsto (fun M : ℕ => {x | (M : ℝ) ≤ ‖f x‖₊}.indicator f x) atTop (𝓝 0) :=
univ_mem' (id fun x => tendsto_indicator_ge f x)
have hmeas : ∀ M : ℕ, AEStronglyMeasurable ({x | (M : ℝ) ≤ ‖f x‖₊}.indicator f) μ :=
by
intro M
apply hf.1.indicator
apply
StronglyMeasurable.measurableSet_le stronglyMeasurable_const
hmeas.nnnorm.measurable.coe_nnreal_real.stronglyMeasurable
have hbound : HasFiniteIntegral (fun x => ‖f x‖) μ :=
by
rw [memLp_one_iff_integrable] at hf
exact hf.norm.2
have : Tendsto (fun n : ℕ ↦ ∫⁻ a, ENNReal.ofReal ‖{x | n ≤ ‖f x‖₊}.indicator f a - 0‖ ∂μ) atTop (𝓝 0) :=
by
refine tendsto_lintegral_norm_of_dominated_convergence hmeas hbound ?_ htendsto
refine fun n => univ_mem' (id fun x => ?_)
by_cases hx : (n : ℝ) ≤ ‖f x‖
· dsimp
rwa [Set.indicator_of_mem]
· dsimp
rw [Set.indicator_of_notMem, norm_zero]
· exact norm_nonneg _
· assumption
rw [ENNReal.tendsto_atTop_zero] at this
obtain ⟨M, hM⟩ := this (ENNReal.ofReal ε) (ENNReal.ofReal_pos.2 hε)
simp only [sub_zero] at hM
refine ⟨M, ?_⟩
convert hM M le_rfl
simp only [coe_nnnorm, ENNReal.ofReal_eq_coe_nnreal (norm_nonneg _)]
rfl
