Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eLpNorm_lorentz_helper

Carleson.ToMathlib.MeasureTheory.Function.LorentzSeminorm.TriangleInequality · Carleson/ToMathlib/MeasureTheory/Function/LorentzSeminorm/TriangleInequality.lean:96 to 145

Mathematical statement

Exact Lean statement

lemma eLpNorm_lorentz_helper (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤)
  (one_le_q : 1 ≤ q) (q_ne_top : q ≠ ⊤)
  (hf : eLorentzNorm' f p q μ ≠ 0) (hf' : eLorentzNorm' f p q μ ≠ ⊤) :
    eLpNorm (lorentz_helper f p q μ) q.conjExponent = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eLpNorm_lorentz_helper (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤)  (one_le_q : 1 ≤ q) (q_ne_top : q ≠ ⊤)  (hf : eLorentzNorm' f p q μ ≠ 0) (hf' : eLorentzNorm' f p q μ ≠ ⊤) :    eLpNorm (lorentz_helper f p q μ) q.conjExponent = 1 := by  have q_ne_zero : q ≠ 0 := by aesop  have q'_ne_zero : q.conjExponent ≠ 0 := (ENNReal.HolderConjugate.conjExponent one_le_q).symm.ne_zero  by_cases q_ne_one : q = 1  · unfold lorentz_helper    rw [q_ne_one]    simp only [ENNReal.toReal_one, sub_self, ENNReal.rpow_zero, ENNReal.toReal_inv, inv_one,      one_smul]    convert eLpNorm_exponent_top    · exact ENNReal.HolderConjugate.conjExponent_eq    rw [eLpNormEssSup_const _ (NeZero.ne volume)]    simp  have q_sub_one : ¬q - 1 = 0 := by    rw [tsub_eq_zero_iff_le]    contrapose! q_ne_one    exact le_antisymm q_ne_one one_le_q  have q'_ne_top : q.conjExponent ≠ ⊤ := (ENNReal.HolderConjugate.conjExponent one_le_q).symm.ne_top_iff_ne_one.mpr q_ne_one  unfold lorentz_helper  rw [eLpNorm_const_smul''' (by fun_prop)]  rw [eLorentzNorm'_eq' p_ne_zero p_ne_top, eLpNorm_eq_lintegral_rpow_enorm_toReal q_ne_zero q_ne_top,      eLpNorm_eq_lintegral_rpow_enorm_toReal q'_ne_zero q'_ne_top] at *  simp only [ENNReal.toReal_inv, enorm_eq_self, one_div] at *  rw [← ENNReal.rpow_mul]  simp_rw [← ENNReal.rpow_mul]  have : ((q.toReal - 1) * q.conjExponent.toReal) = q.toReal := by    rw [ENNReal.conjExponent, ENNReal.toReal_add (by simp)          (by simp only [ne_eq, ENNReal.inv_eq_top]; assumption),        ENNReal.toReal_inv, ENNReal.toReal_sub_of_le one_le_q q_ne_top]    simp only [ENNReal.toReal_one]    rw [mul_add, mul_one, mul_inv_cancel₀, sub_add_cancel]    contrapose! q_ne_one    rw [sub_eq_zero] at q_ne_one    rw [← ENNReal.ofReal_toReal q_ne_top, q_ne_one, ENNReal.ofReal_one]  rw [this]  rw [← ENNReal.rpow_add]  · convert ENNReal.rpow_zero    rw [ENNReal.conjExponent, ENNReal.toReal_add (by simp)          (by simp only [ne_eq, ENNReal.inv_eq_top]; assumption),        ENNReal.toReal_inv, ENNReal.toReal_sub_of_le one_le_q q_ne_top]    simp only [ENNReal.toReal_one]    grind  · contrapose! hf    rw [hf, ENNReal.zero_rpow_of_pos]    exact inv_pos.mpr (ENNReal.toReal_pos q_ne_zero q_ne_top)  · contrapose! hf'    rw [hf', ENNReal.top_rpow_of_pos]    exact inv_pos.mpr (ENNReal.toReal_pos q_ne_zero q_ne_top)