α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
have hq0_lt : 0 < q := lt_of_lt_of_le hp0_lt hpq
case pos
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)

case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
by_cases hpq_eq : p = q
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
have hpq : p < q := lt_of_le_of_ne hpq hpq_eq
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
let g := fun _ : α => (1 : ℝ≥0∞)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
have h_rw : (∫⁻ a, (‖f a‖₊ : ℝ≥0∞) ^ p ∂μ) = ∫⁻ a, ((‖f a‖₊ : ℝ≥0∞) * g a) ^ p ∂μ :=
  lintegral_congr fun a => by simp
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
repeat' rw [snorm']
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
rw [h_rw]
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
⊢ (∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
let r := p * q / (q - p)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
⊢ (∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
have hpqr : 1 / p = 1 / q + 1 / r := by
  field_simp [(ne_of_lt hp0_lt).symm, (ne_of_lt hq0_lt).symm]
  ring
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
calc
  (∫⁻ a : α, (↑‖f a‖₊ * g a) ^ p ∂μ) ^ (1 / p) ≤
      (∫⁻ a : α, ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) :=
    ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hf.ennnorm aemeasurable_const
  _ = (∫⁻ a : α, ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q) := by
    rw [hpqr]; simp
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : p = q
⊢ snorm' f p μ ≤ snorm' f q μ * ↑↑μ Set.univ ^ (1 / p - 1 / q)
rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
a : α
⊢ ↑‖f a‖₊ ^ p = (↑‖f a‖₊ * g a) ^ p
simp
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
rw [snorm']
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
⊢ p * q = q * p
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
⊢ 1 / p = 1 / q + 1 / r
field_simp [(ne_of_lt hp0_lt).symm, (ne_of_lt hq0_lt).symm]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
⊢ p * q = q * p
ring
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / q + 1 / r - 1 / q)
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / p - 1 / q)
rw [hpqr]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.3186605
G : Type ?u.3186608
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q✝ : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p q : ℝ
hp0_lt : 0 < p
hpq✝ : p ≤ q
f : α → E
hf : AEStronglyMeasurable f μ
hq0_lt : 0 < q
hpq_eq : ¬p = q
hpq : p < q
g : α → ℝ≥0∞ := fun x => 1
h_rw : (∫⁻ (a : α), ↑‖f a‖₊ ^ p ∂μ) = ∫⁻ (a : α), (↑‖f a‖₊ * g a) ^ p ∂μ
r : ℝ := p * q / (q - p)
hpqr : 1 / p = 1 / q + 1 / r
⊢ (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r) =
    (∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ) ^ (1 / q) * ↑↑μ Set.univ ^ (1 / q + 1 / r - 1 / q)
simp