Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.C_realInterpolation_ENNReal_pos

Carleson.ToMathlib.RealInterpolation.Main · Carleson/ToMathlib/RealInterpolation/Main.lean:1339 to 1367

Mathematical statement

Exact Lean statement

lemma C_realInterpolation_ENNReal_pos {p₀ p₁ q₀ q₁ q : ℝ≥0∞} {A : ℝ≥0} (hA : 0 < A)
    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁)
    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)
    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁) :
    0 < C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma C_realInterpolation_ENNReal_pos {p₀ p₁ q₀ q₁ q : ℝ≥0∞} {A : ℝ≥0} (hA : 0 < A)    (hp₀ : p₀ ∈ Ioc 0 q₀) (hp₁ : p₁ ∈ Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁)    {C₀ C₁ : ℝ≥0} (ht : t ∈ Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁)    (hq : q⁻¹ = (1 - t) / q₀ + t / q₁) :    0 < C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t := by  have q₀pos : 0 < q₀ := pos_of_rb_Ioc hp₀  have q₁pos : 0 < q₁ := pos_of_rb_Ioc hp₁  unfold C_realInterpolation_ENNReal  apply ENNReal.mul_pos  · apply mul_ne_zero    · apply mul_ne_zero      · apply mul_ne_zero        · split_ifs <;> positivity        · apply ne_of_gt          apply ENNReal.rpow_pos          · exact interpolated_pos' q₀pos q₁pos (ne_top_of_Ioo ht) hq          · exact interp_exp_ne_top hq₀q₁ ht hq      · apply ne_of_gt        apply ENNReal.rpow_pos ?_ (by finiteness)        split_ifs        · rw [one_mul, one_mul]          apply add_pos'          · exact ofReal_inv_interp_sub_exp_pos₁ ht q₀pos q₁pos hq₀q₁ hq          · exact ofReal_inv_interp_sub_exp_pos₀ ht q₀pos q₁pos hq₀q₁ hq        · simp [ofReal_inv_interp_sub_exp_pos₁ ht q₀pos q₁pos hq₀q₁ hq]        · simp [ofReal_inv_interp_sub_exp_pos₀ ht q₀pos q₁pos hq₀q₁ hq]        · simp_all    · exact (ENNReal.rpow_pos (by positivity) coe_ne_top).ne'  · exact (ENNReal.rpow_pos (by positivity) coe_ne_top).ne'