Source indexedlemma · leanprover/lean4:v4.32.0

eLpNorm_czRemainder_le

Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:994 to 1007

Source documentation

Part of Lemma 10.2.5, equation (10.2.21) (finite case).

Exact Lean statement

lemma eLpNorm_czRemainder_le {hf : BoundedFiniteSupport f}
    (hX : ¬ GeneralCase f α) (hα : ⨍⁻ x, ‖f x‖ₑ < α) :
    eLpNorm (czRemainder f α) 1 volume ≤ 2 ^ (2 * a + 1) * α * volume (univ : Set X)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_czRemainder_le {hf : BoundedFiniteSupport f}    (hX : ¬ GeneralCase f α) (hα : ⨍⁻ x, ‖f x‖ₑ < α) :    eLpNorm (czRemainder f α) 1 volume ≤ 2 ^ (2 * a + 1) * α * volume (univ : Set X) := by  by_cases h : Nonempty X; swap  · have := not_nonempty_iff.mp h; simp  have := isFiniteMeasure_of_not_generalCase hf hX (lt_of_le_of_lt zero_le hα)  calc    _ ≤ 2 * ∫⁻ x, ‖f x‖ₑ := eLpNorm_czRemainder_le' hf hX hα    _ ≤ 2 * (α * volume (univ : Set X)) := by      rw [laverage_eq] at hα      exact mul_le_mul_right (a := 2) <| ENNReal.div_lt_iff (Or.inl (NeZero.ne _))        (Or.inl this.measure_univ_lt_top.ne) |>.mp hα |>.le    _ ≤ 2 ^ (2 * a + 1) * α * volume (univ : Set X) := by      rw [← mul_assoc]; gcongr; simpa using pow_le_pow_right' one_le_two (Nat.le_add_left 1 (2 * a))