α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hp0_ne : p ≠ 0 := (ne_of_lt hp0_lt).symm
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hp0 : 0 ≤ p := le_of_lt hp0_lt
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hq0_lt : 0 < q := lt_of_le_of_lt hp0 hpq
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hq0_ne : q ≠ 0 := (ne_of_lt hq0_lt).symm
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have h_one_div_r : 1 / r = 1 / p - 1 / q := by rw [hpqr]; simp
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have _ : r ≠ 0 := by
  have hr_inv_pos : 0 < 1 / r := by rwa [h_one_div_r, sub_pos, one_div_lt_one_div hq0_lt hp0_lt]
  rw [one_div, _root_.inv_pos] at hr_inv_pos
  exact (ne_of_lt hr_inv_pos).symm
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
let p2 := q / p
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
let q2 := p2.conjugateExponent
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hp2q2 : p2.IsConjugateExponent q2 :=
  Real.isConjugateExponent_conjugateExponent (by simp [_root_.lt_div_iff, hpq, hp0_lt])
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
calc
  (∫⁻ a : α, (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ a : α, f a ^ p * g a ^ p ∂μ) ^ (1 / p) := by
    simp_rw [Pi.mul_apply, ENNReal.mul_rpow_of_nonneg _ _ hp0]
  _ ≤ ((∫⁻ a, f a ^ (p * p2) ∂μ) ^ (1 / p2) *
      (∫⁻ a, g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) := by
    refine' ENNReal.rpow_le_rpow _ (by simp [hp0])
    simp_rw [ENNReal.rpow_mul]
    exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)
  _ = (∫⁻ a : α, f a ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) := by
    rw [@ENNReal.mul_rpow_of_nonneg _ _ (1 / p) (by simp [hp0]), ← ENNReal.rpow_mul, ←
      ENNReal.rpow_mul]
    have hpp2 : p * p2 = q := by
      symm
      rw [mul_comm, ← div_eq_iff hp0_ne]
    have hpq2 : p * q2 = r := by
      rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
      field_simp [Real.conjugateExponent, hp0_ne, hq0_ne]
    simp_rw [div_mul_div_comm, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ 1 / r = 1 / q + 1 / r - 1 / q
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ 1 / r = 1 / p - 1 / q
rw [hpqr]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
⊢ 1 / r = 1 / q + 1 / r - 1 / q
simp
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
hr_inv_pos : 0 < 1 / r
⊢ r ≠ 0
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
⊢ r ≠ 0
have hr_inv_pos : 0 < 1 / r := by rwa [h_one_div_r, sub_pos, one_div_lt_one_div hq0_lt hp0_lt]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
hr_inv_pos : 0 < r
⊢ r ≠ 0
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
hr_inv_pos : 0 < 1 / r
⊢ r ≠ 0
rw [one_div, _root_.inv_pos] at hr_inv_pos
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
hr_inv_pos : 0 < r
⊢ r ≠ 0
exact (ne_of_lt hr_inv_pos).symm
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
⊢ 0 < 1 / r
rwa [h_one_div_r, sub_pos, one_div_lt_one_div hq0_lt hp0_lt]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
⊢ 1 < p2
simp [_root_.lt_div_iff, hpq, hp0_lt]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) = (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ^ (1 / p)
simp_rw [Pi.mul_apply, ENNReal.mul_rpow_of_nonneg _ _ hp0]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ≤
    (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ^ (1 / p) ≤
    ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p)
refine' ENNReal.rpow_le_rpow _ (by simp [hp0])
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ≤
    (∫⁻ (a : α), (f a ^ p) ^ (q / p) ∂μ) ^ (1 / (q / p)) *
      (∫⁻ (a : α), (g a ^ p) ^ Real.conjugateExponent (q / p) ∂μ) ^ (1 / Real.conjugateExponent (q / p))
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ≤
    (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)
simp_rw [ENNReal.rpow_mul]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ p * g a ^ p ∂μ) ≤
    (∫⁻ (a : α), (f a ^ p) ^ (q / p) ∂μ) ^ (1 / (q / p)) *
      (∫⁻ (a : α), (g a ^ p) ^ Real.conjugateExponent (q / p) ∂μ) ^ (1 / Real.conjugateExponent (q / p))
exact ENNReal.lintegral_mul_le_Lp_mul_Lq μ hp2q2 (hf.pow_const _) (hg.pow_const _)
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ 0 ≤ 1 / p
simp [hp0]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2 * (1 / p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ ((∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2)) ^ (1 / p) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
rw [@ENNReal.mul_rpow_of_nonneg _ _ (1 / p) (by simp [hp0]), ← ENNReal.rpow_mul, ←
  ENNReal.rpow_mul]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2 * (1 / p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2 * (1 / p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hpp2 : p * p2 = q := by
  symm
  rw [mul_comm, ← div_eq_iff hp0_ne]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2 * (1 / p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2 * (1 / p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
have hpq2 : p * q2 = r := by
  rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
  field_simp [Real.conjugateExponent, hp0_ne, hq0_ne]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
hpq2 : p * q2 = r
⊢ (∫⁻ (a : α), f a ^ (p * p2) ∂μ) ^ (1 / p2 * (1 / p)) * (∫⁻ (a : α), g a ^ (p * q2) ∂μ) ^ (1 / q2 * (1 / p)) =
    (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
simp_rw [div_mul_div_comm, mul_one, mul_comm p2, mul_comm q2, hpp2, hpq2]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ 0 ≤ 1 / p
simp [hp0]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ q = p * p2
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ p * p2 = q
symm
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
⊢ q = p * p2
rw [mul_comm, ← div_eq_iff hp0_ne]
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
⊢ p * q2 = 1 / (1 / p - 1 / q)
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
⊢ p * q2 = r
rw [← inv_inv r, ← one_div, ← one_div, h_one_div_r]
no goals
α✝ : Type ?u.1456644
inst✝¹ : MeasurableSpace α✝
μ✝ : MeasureTheory.Measure α✝
α : Type u_1
inst✝ : MeasurableSpace α
p q r : ℝ
hp0_lt : 0 < p
hpq : p < q
hpqr : 1 / p = 1 / q + 1 / r
μ : MeasureTheory.Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f
hg : AEMeasurable g
hp0_ne : p ≠ 0
hp0 : 0 ≤ p
hq0_lt : 0 < q
hq0_ne : q ≠ 0
h_one_div_r : 1 / r = 1 / p - 1 / q
x✝ : r ≠ 0
p2 : ℝ := q / p
q2 : ℝ := Real.conjugateExponent p2
hp2q2 : Real.IsConjugateExponent p2 q2
hpp2 : p * p2 = q
⊢ p * q2 = 1 / (1 / p - 1 / q)
field_simp [Real.conjugateExponent, hp0_ne, hq0_ne]