Source indexedlemma · leanprover/lean4:v4.32.0

ENNReal.le_on_subset

Carleson.Classical.ControlApproximationEffectBasic · Carleson/Classical/ControlApproximationEffectBasic.lean:22 to 61

Mathematical statement

Exact Lean statement

lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g : X → ℝ≥0∞}
    {E : Set X} (hE : MeasurableSet E)
    (hf : Measurable f) (hg : Measurable g) {a : ℝ≥0∞} (h : ∀ x ∈ E, a ≤ f x + g x) :
    ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E'
      ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ (∀ x ∈ E', a / 2 ≤ g x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ENNReal.le_on_subset {X : Type} [MeasurableSpace X] (μ : Measure X) {f g : X → ℝ≥0∞}    {E : Set X} (hE : MeasurableSet E)    (hf : Measurable f) (hg : Measurable g) {a : ℝ≥0∞} (h : ∀ x ∈ E, a ≤ f x + g x) :    ∃ E' ⊆ E, MeasurableSet E' ∧ μ E ≤ 2 * μ E'      ∧ ((∀ x ∈ E', a / 2 ≤ f x) ∨ (∀ x ∈ E', a / 2 ≤ g x)) := by  set Ef := E ∩ f⁻¹' (Set.Ici (a / 2)) with Ef_def  set Eg := E ∩ g⁻¹' (Set.Ici (a / 2)) with Eg_def  have : E ⊆ Ef ∪ Eg := by    intro x hx    rw [Ef_def, Eg_def]    simp only [Set.mem_union, Set.mem_inter_iff, Set.mem_preimage, Set.mem_Ici]    by_contra! hx'    absurd le_refl a    push Not    calc a      _ ≤ f x + g x := h x hx      _ < a / 2 + a / 2 := by        exact ENNReal.add_lt_add (hx'.1 hx) (hx'.2 hx)      _ = a := by        ring_nf        apply ENNReal.div_mul_cancel <;> norm_num  have : μ E ≤ 2 * μ Ef ∨ μ E ≤ 2 * μ Eg := by    by_contra! hEfg    absurd le_refl (2 * μ E)    push Not    calc 2 * μ E    _ ≤ 2 * μ (Ef ∪ Eg) := by      gcongr    _ ≤ 2 * (μ Ef + μ Eg) := by      gcongr      exact measure_union_le _ _    _ = 2 * μ Ef + 2 * μ Eg := by ring    _ < μ E + μ E := by      exact ENNReal.add_lt_add hEfg.1 hEfg.2    _ = 2 * μ E := by ring  rcases this with hEf | hEg  · refine ⟨Ef, Set.inter_subset_left, hE.inter (hf measurableSet_Ici), hEf, Or.inl ?_⟩    simp [Ef_def]  · refine ⟨Eg, Set.inter_subset_left, hE.inter (hg measurableSet_Ici), hEg, Or.inr ?_⟩    simp [Eg_def]