English
Equationally compatible between the subtype structure and the ambient action on Lp under multiplicative actions.
Русский
Эквивалентность между структурой подмножества и внешним действием на Lp при умножающих действиях.
LaTeX
$$Eq (DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp ...)$$
Lean4
/-- The `eLpNorm` of the indicator of a set is uniformly small if the set itself has small measure,
for any `p < ∞`. Given here as an existential `∀ ε > 0, ∃ η > 0, ...` to avoid later
management of `ℝ≥0∞`-arithmetic. -/
theorem exists_eLpNorm_indicator_le (hp : p ≠ ∞) (c : E) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _ => c) p μ ≤ ε :=
by
rcases eq_or_ne p 0 with (rfl | h'p)
· exact ⟨1, zero_lt_one, fun s _ => by simp⟩
have hp₀ : 0 < p := bot_lt_iff_ne_bot.2 h'p
have hp₀' : 0 ≤ 1 / p.toReal := div_nonneg zero_le_one ENNReal.toReal_nonneg
have hp₀'' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
obtain ⟨η, hη_pos, hη_le⟩ : ∃ η : ℝ≥0, 0 < η ∧ ‖c‖ₑ * (η : ℝ≥0∞) ^ (1 / p.toReal) ≤ ε :=
by
have : Filter.Tendsto (fun x : ℝ≥0 => ((‖c‖₊ * x ^ (1 / p.toReal) : ℝ≥0) : ℝ≥0∞)) (𝓝 0) (𝓝 (0 : ℝ≥0)) :=
by
rw [ENNReal.tendsto_coe]
convert (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _
simp [hp₀''.ne']
have hε' : 0 < ε := hε.bot_lt
obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε')
obtain ⟨η, hη, hηδ⟩ := exists_between hδ
refine ⟨η, hη, ?_⟩
simpa only [← ENNReal.coe_rpow_of_nonneg _ hp₀', enorm, ← ENNReal.coe_mul] using hδε' hηδ
refine ⟨η, hη_pos, fun s hs => ?_⟩
refine (eLpNorm_indicator_const_le _ _).trans (le_trans ?_ hη_le)
exact mul_le_mul_left' (ENNReal.rpow_le_rpow hs hp₀') _
