English
Membership in insert a s is equivalent to x equals a or x belongs to s.
Русский
Принадлежность к вставке a в s эквивалентна тому, что x равен a или x принадлежит s.
LaTeX
$$$$x\\in (insert\\;a\\;s) \\iff x=a \\;\\lor\\; x\\in s.$$$$
Lean4
/-- If a set of ae strongly measurable functions is stable under addition and approximates
characteristic functions in `ℒp`, then it is dense in `ℒp`. -/
theorem induction_dense (hp_ne_top : p ≠ ∞) (P : (α → E) → Prop)
(h0P :
∀ (c : E) ⦃s : Set α⦄,
MeasurableSet s →
μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g : α → E, eLpNorm (g - s.indicator fun _ => c) p μ ≤ ε ∧ P g)
(h1P : ∀ f g, P f → P g → P (f + g)) (h2P : ∀ f, P f → AEStronglyMeasurable f μ) {f : α → E} (hf : MemLp f p μ)
{ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ g : α → E, eLpNorm (f - g) p μ ≤ ε ∧ P g :=
by
rcases eq_or_ne p 0 with (rfl | hp_pos)
· rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top]) hε with ⟨g, _, Pg⟩
exact ⟨g, by simp only [eLpNorm_exponent_zero, zero_le'], Pg⟩
suffices H : ∀ (f' : α →ₛ E) (δ : ℝ≥0∞) (hδ : δ ≠ 0), MemLp f' p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
by
obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p hε
rcases hf.exists_simpleFunc_eLpNorm_sub_lt hp_ne_top ηpos.ne' with ⟨f', hf', f'_mem⟩
rcases H f' η ηpos.ne' f'_mem with ⟨g, hg, Pg⟩
refine ⟨g, ?_, Pg⟩
convert
(hη _ _ (hf.aestronglyMeasurable.sub f'.aestronglyMeasurable) (f'.aestronglyMeasurable.sub (h2P g Pg)) hf'.le
hg).le using
2
simp only [sub_add_sub_cancel]
apply SimpleFunc.induction
· intro c s hs ε εpos Hs
rcases eq_or_ne c 0 with (rfl | hc)
· rcases h0P (0 : E) MeasurableSet.empty (by simp only [measure_empty, zero_lt_top]) εpos with ⟨g, hg, Pg⟩
rw [← eLpNorm_neg, neg_sub] at hg
refine ⟨g, ?_, Pg⟩
convert hg
ext x
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_zero, piecewise_eq_indicator,
indicator_zero', Pi.zero_apply, indicator_zero]
· have : μ s < ∞ := SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs Hs
rcases h0P c hs this εpos with ⟨g, hg, Pg⟩
rw [← eLpNorm_neg, neg_sub] at hg
exact ⟨g, hg, Pg⟩
· intro f f' hff' hf hf' δ δpos int_ff'
obtain ⟨η, ηpos, hη⟩ := exists_Lp_half E μ p δpos
rw [SimpleFunc.coe_add, memLp_add_of_disjoint hff' f.stronglyMeasurable f'.stronglyMeasurable] at int_ff'
rcases hf η ηpos.ne' int_ff'.1 with ⟨g, hg, Pg⟩
rcases hf' η ηpos.ne' int_ff'.2 with ⟨g', hg', Pg'⟩
refine ⟨g + g', ?_, h1P g g' Pg Pg'⟩
convert (hη _ _ (f.aestronglyMeasurable.sub (h2P g Pg)) (f'.aestronglyMeasurable.sub (h2P g' Pg')) hg hg').le using
2
rw [SimpleFunc.coe_add]
abel
