case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ

case neg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
by_cases hp_top : p = ∞
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : p = 0
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ

case neg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
case neg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
by_cases hp_zero : p = 0
case neg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖b (f x) (g x)‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
case neg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
simp_rw [snorm_eq_lintegral_rpow_nnnorm hp_zero hp_top, snorm_exponent_top, snormEssSup]
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
⊢ snormEssSup (fun x => b (f x) (g x)) μ ≤ snormEssSup f μ * snormEssSup g μ
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
simp_rw [hp_top, snorm_exponent_top]
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ (fun x => ↑‖(fun x => b (f x) (g x)) x‖₊) a ≤ ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
⊢ snormEssSup (fun x => b (f x) (g x)) μ ≤ snormEssSup f μ * snormEssSup g μ
refine' le_trans (essSup_mono_ae <| h.mono fun a ha => _) (ENNReal.essSup_mul_le _ _)
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ (fun x => ↑‖(fun x => b (f x) (g x)) x‖₊) a ≤ ((fun x => ↑‖f x‖₊) * fun x => ↑‖g x‖₊) a
simp_rw [Pi.mul_apply, ← ENNReal.coe_mul, ENNReal.coe_le_coe]
no goals
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : p = ⊤
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
exact ha
no goals
case pos
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : p = 0
⊢ snorm (fun x => b (f x) (g x)) p μ ≤ snorm f ⊤ μ * snorm g p μ
simp only [hp_zero, snorm_exponent_zero, MulZeroClass.mul_zero, le_zero_iff]
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖b (f x) (g x)‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖b (f x) (g x)‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤
    (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
refine' ENNReal.rpow_le_rpow _ (one_div_nonneg.mpr ENNReal.toReal_nonneg)
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ↑‖b (f a) (g a)‖₊ ^ ENNReal.toReal p ≤ ↑‖f a‖₊ ^ ENNReal.toReal p * ↑‖g a‖₊ ^ ENNReal.toReal p
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖b (f x) (g x)‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ
refine' lintegral_mono_ae (h.mono fun a ha => _)
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ↑‖b (f a) (g a)‖₊ ^ ENNReal.toReal p ≤ (↑‖f a‖₊ * ↑‖g a‖₊) ^ ENNReal.toReal p
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ↑‖b (f a) (g a)‖₊ ^ ENNReal.toReal p ≤ ↑‖f a‖₊ ^ ENNReal.toReal p * ↑‖g a‖₊ ^ ENNReal.toReal p
rw [← ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg]
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ↑‖b (f a) (g a)‖₊ ≤ ↑‖f a‖₊ * ↑‖g a‖₊
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ↑‖b (f a) (g a)‖₊ ^ ENNReal.toReal p ≤ (↑‖f a‖₊ * ↑‖g a‖₊) ^ ENNReal.toReal p
refine' ENNReal.rpow_le_rpow _ ENNReal.toReal_nonneg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ↑‖b (f a) (g a)‖₊ ≤ ↑‖f a‖₊ * ↑‖g a‖₊
rw [← ENNReal.coe_mul, ENNReal.coe_le_coe]
no goals
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
a : α
ha : ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
⊢ ‖b (f a) (g a)‖₊ ≤ ‖f a‖₊ * ‖g a‖₊
exact ha
case refine'_1
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ∫⁻ (x : α), essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ

case refine'_2
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤
    (∫⁻ (x : α), essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p)
refine' ENNReal.rpow_le_rpow _ _
case refine'_2
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p

case refine'_1
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ∫⁻ (x : α), essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ
case refine'_1
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ∫⁻ (x : α), essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ

case refine'_2
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p
swap
case refine'_1
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ ∀ᵐ (a : α) ∂μ,
    ↑‖f a‖₊ ^ ENNReal.toReal p * ↑‖g a‖₊ ^ ENNReal.toReal p ≤
      essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g a‖₊ ^ ENNReal.toReal p
case refine'_1
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ≤
    ∫⁻ (x : α), essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ
refine' lintegral_mono_ae _
case h
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
x : α
hx : ↑‖f x‖₊ ≤ essSup (fun x => ↑‖f x‖₊) μ
⊢ ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ≤
    essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p
case refine'_1
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ ∀ᵐ (a : α) ∂μ,
    ↑‖f a‖₊ ^ ENNReal.toReal p * ↑‖g a‖₊ ^ ENNReal.toReal p ≤
      essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g a‖₊ ^ ENNReal.toReal p
filter_upwards [@ENNReal.ae_le_essSup _ _ μ fun x => (‖f x‖₊ : ℝ≥0∞)]with x hx
no goals
case h
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
x : α
hx : ↑‖f x‖₊ ≤ essSup (fun x => ↑‖f x‖₊) μ
⊢ ↑‖f x‖₊ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ≤
    essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p
exact mul_le_mul_right' (ENNReal.rpow_le_rpow hx ENNReal.toReal_nonneg) _
case refine'_2
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ ENNReal.toReal p
case refine'_2
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p
rw [one_div_nonneg]
no goals
case refine'_2
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ ENNReal.toReal p
exact ENNReal.toReal_nonneg
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)

case hf
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ AEMeasurable fun x => ↑‖g x‖₊ ^ ENNReal.toReal p
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (∫⁻ (x : α), essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
rw [lintegral_const_mul'']
case hf
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ AEMeasurable fun x => ↑‖g x‖₊ ^ ENNReal.toReal p

α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)

case hf
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ AEMeasurable fun x => ↑‖g x‖₊ ^ ENNReal.toReal p
swap
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)

case hz
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p * ∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^
      (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
rw [ENNReal.mul_rpow_of_nonneg]
case hz
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p

α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)

case hz
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p
swap
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ ENNReal.toReal p ≠ 0
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ (essSup (fun x => ↑‖f x‖₊) μ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (a : α), ↑‖g a‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) =
    essSup (fun x => ↑‖f x‖₊) μ * (∫⁻ (x : α), ↑‖g x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p)
rw [← ENNReal.rpow_mul, one_div, mul_inv_cancel, ENNReal.rpow_one]
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ ¬p = 0 ∧ ¬p = ⊤
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ ENNReal.toReal p ≠ 0
rw [Ne.def, ENNReal.toReal_eq_zero_iff, not_or]
no goals
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ ¬p = 0 ∧ ¬p = ⊤
exact ⟨hp_zero, hp_top⟩
no goals
case hf
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ AEMeasurable fun x => ↑‖g x‖₊ ^ ENNReal.toReal p
exact hg.nnnorm.aemeasurable.coe_nnreal_ennreal.pow aemeasurable_const
case hz
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ ENNReal.toReal p
case hz
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ 1 / ENNReal.toReal p
rw [one_div_nonneg]
no goals
case hz
α : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
hp_top : ¬p = ⊤
hp_zero : ¬p = 0
⊢ 0 ≤ ENNReal.toReal p
exact ENNReal.toReal_nonneg