Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq (ForML/LpHoelder.lean)

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
⊢ ‖L1_of_mul hpq f g‖ ≤ ‖f‖ * ‖g‖
Tactic:
generalize hξ : L1_of_mul hpq f g = ξ
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ ‖ξ‖ ≤ ‖f‖ * ‖g‖

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ ‖ξ‖ ≤ ‖f‖ * ‖g‖
Tactic:
simp [Lp.norm_def]
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ ENNReal.toReal (snorm (↑↑ξ) 1 μ) ≤ ENNReal.toReal (snorm (↑↑f) p μ) * ENNReal.toReal (snorm (↑↑g) q μ)

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ ENNReal.toReal (snorm (↑↑ξ) 1 μ) ≤ ENNReal.toReal (snorm (↑↑f) p μ) * ENNReal.toReal (snorm (↑↑g) q μ)
Tactic:
rw [← ENNReal.toReal_mul]
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ ENNReal.toReal (snorm (↑↑ξ) 1 μ) ≤ ENNReal.toReal (snorm (↑↑f) p μ * snorm (↑↑g) q μ)

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ ENNReal.toReal (snorm (↑↑ξ) 1 μ) ≤ ENNReal.toReal (snorm (↑↑f) p μ * snorm (↑↑g) q μ)
Tactic:
rw [ENNReal.toReal_le_toReal]
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤
Tactic:
rotate_left
State after:
case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

State before:
case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
. exact Lp.snorm_ne_top _
State after:
case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

State before:
case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
. exact ENNReal.mul_ne_top (Lp.snorm_ne_top _) (Lp.snorm_ne_top _)
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
rw [← hξ]
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑(L1_of_mul hpq f g)) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑(L1_of_mul hpq f g)) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
rw [snorm_congr_ae (coeFn_L1_of_mul hpq)]
State after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f * ↑↑g) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

State before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f * ↑↑g) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
refine snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq hpq ?_ ?_
State after:
case refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ

case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ

State before:
case refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ

case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
. exact (Lp.memℒp f).aestronglyMeasurable
State after:
case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ

State before:
case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
. exact (Lp.memℒp g).aestronglyMeasurable
State after:
no goals

State before:
case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤
Tactic:
exact Lp.snorm_ne_top _
State after:
no goals

State before:
case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤
Tactic:
exact ENNReal.mul_ne_top (Lp.snorm_ne_top _) (Lp.snorm_ne_top _)
State after:
no goals

State before:
case refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ
Tactic:
exact (Lp.memℒp f).aestronglyMeasurable
State after:
no goals

State before:
case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
exact (Lp.memℒp g).aestronglyMeasurable
State after:
no goals