α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
by_cases hf_top : (∫⁻ a, f a ^ p ∂μ) = ⊤
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : (∫⁻ (a : α), g a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
by_cases hg_top : (∫⁻ a, g a ^ p ∂μ) = ⊤
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
by_cases h1 : p = 1
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have hp1_lt : 1 < p := by
  refine' lt_of_le_of_ne hp1 _
  symm
  exact h1
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have hpq := Real.isConjugateExponent_conjugateExponent hp1_lt
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : (∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
htop : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have htop : (∫⁻ a, (f + g) a ^ p ∂μ) ≠ ⊤ := by
  rw [← Ne.def] at hf_top hg_top
  rw [← lt_top_iff_ne_top] at hf_top hg_top⊢
  exact lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1
no goals
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
htop : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≠ ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
exact lintegral_Lp_add_le_aux hpq hf hf_top hg hg_top h0 htop
no goals
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
simp [hf_top, hp_pos]
no goals
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : (∫⁻ (a : α), g a ^ p ∂μ) = ⊤
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
simp [hg_top, hp_pos]
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
refine' le_of_eq _
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
simp_rw [h1, one_div_one, ENNReal.rpow_one]
no goals
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : p = 1
⊢ (∫⁻ (a : α), (f + g) a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
exact lintegral_add_left' hf _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ 1 ≠ p
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ 1 < p
refine' lt_of_le_of_ne hp1 _
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ p ≠ 1
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ 1 ≠ p
symm
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
⊢ p ≠ 1
exact h1
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : (∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ 0 ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : (∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rw [h0, @ENNReal.zero_rpow_of_pos (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
no goals
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : (∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ 0 ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
exact zero_le _
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : (∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ 0 < 1 / p
simp [lt_of_lt_of_le zero_lt_one hp1]
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
hg_top : (∫⁻ (a : α), g a ^ p ∂μ) ≠ ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≠ ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ¬(∫⁻ (a : α), f a ^ p ∂μ) = ⊤
hg_top : ¬(∫⁻ (a : α), g a ^ p ∂μ) = ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≠ ⊤
rw [← Ne.def] at hf_top hg_top
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) < ⊤
hg_top : (∫⁻ (a : α), g a ^ p ∂μ) < ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) < ⊤
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) ≠ ⊤
hg_top : (∫⁻ (a : α), g a ^ p ∂μ) ≠ ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ≠ ⊤
rw [← lt_top_iff_ne_top] at hf_top hg_top⊢
no goals
α : Type u_1
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : (∫⁻ (a : α), f a ^ p ∂μ) < ⊤
hg_top : (∫⁻ (a : α), g a ^ p ∂μ) < ⊤
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
h0 : ¬(∫⁻ (a : α), (f + g) a ^ p ∂μ) = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) < ⊤
exact lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top hf hf_top hg_top hp1