Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.estimate_norm_rpow_range_operator

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:424 to 436

Mathematical statement

Exact Lean statement

lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁}
    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] [TopologicalSpace E₂] [ContinuousENorm E₂]
    (hq : 0 < q) (tc : StrictRangeToneCouple) {A : ℝ≥0} (hA : 0 < A)
    (ht : SubadditiveTrunc T A f ν) (hTf : AEStronglyMeasurable (T f) ν) :
  ∫⁻ x : α', ‖T f x‖ₑ ^ q ∂ν ≤
  ENNReal.ofReal ((2 * A)^q * q) * ∫⁻ s, distribution (T (trunc f (tc.ton s))) s ν * s^(q - 1) +
  distribution (T (truncCompl f (tc.ton s))) s ν * s ^ (q - 1)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma estimate_norm_rpow_range_operator {q : ℝ} {f : α → E₁}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁] [TopologicalSpace E₂] [ContinuousENorm E₂]    (hq : 0 < q) (tc : StrictRangeToneCouple) {A : ℝ≥0} (hA : 0 < A)    (ht : SubadditiveTrunc T A f ν) (hTf : AEStronglyMeasurable (T f) ν) :  ∫⁻ x : α', ‖T f x‖ₑ ^ q ∂ν ≤  ENNReal.ofReal ((2 * A)^q * q) * ∫⁻ s, distribution (T (trunc f (tc.ton s))) s ν * s^(q - 1) +  distribution (T (truncCompl f (tc.ton s))) s ν * s ^ (q - 1) := by  rw [rewrite_norm_func hq hA hTf]  refine mul_le_mul' (le_refl _) (lintegral_mono_ae ?_)  filter_upwards [ae_in_Ioo_zero_top] with a ha  rw [ENNReal.ofReal_mul (by simp), ← add_mul]  gcongr ?_ * _  convert! estimate_distribution_subadditiveTrunc (tc.ran_ton a ha).1 ht <;> simp