internlm/Lean-Github huggingface dataset:
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤
Tactic:
rotate_left
Proof state after:
case ha
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
case ha
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
. exact Lp.snorm_ne_top _
Proof state after:
case hb
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
case hb
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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 _)
Proof state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
rw [← hξ]
Proof state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑(L1_of_Lp_smul_Lq hpq f g)) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑(L1_of_Lp_smul_Lq hpq f g)) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
rw [snorm_congr_ae (coeFn_L1_of_Lp_smul_Lq hpq)]
Proof state after:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑f • ↑↑g) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑f • ↑↑g) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
refine snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq hpq ?_ ?_
Proof 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
. exact (Lp.memℒp f).aestronglyMeasurable
Proof 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
. exact (Lp.memℒp g).aestronglyMeasurable
Proof state after:
no goals
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
case ha
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤
Tactic:
exact Lp.snorm_ne_top _
Proof state after:
no goals
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof state before:
case hb
E : Type u_1
inst✝⁴ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤
Tactic:
exact ENNReal.mul_ne_top (Lp.snorm_ne_top _) (Lp.snorm_ne_top _)
Proof state after:
no goals
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ
Tactic:
exact (Lp.memℒp f).aestronglyMeasurable
Proof state after:
no goals
Theorem: norm_L1_of_smul_le_norm_Lp_mul_norm_Lq
Proof 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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : ↥(Lp 𝕜 p)
g : ↥(Lp F q)
ξ : ↥(Lp F 1)
hξ : L1_of_Lp_smul_Lq hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
exact (Lp.memℒp g).aestronglyMeasurable
Proof state after:
no goals
Theorem: memL1_Lp_mul_Lq
Proof state before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ Memℒp (f * g) 1
Tactic:
refine And.intro ?_ ?_
Proof 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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable (f * g) μ

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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm (f * g) 1 μ < ⊤
Theorem: memL1_Lp_mul_Lq
Proof 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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable (f * g) μ

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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm (f * g) 1 μ < ⊤
Tactic:
. exact AEStronglyMeasurable.mul hf.aestronglyMeasurable hg.aestronglyMeasurable
Proof 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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm (f * g) 1 μ < ⊤
Theorem: memL1_Lp_mul_Lq
Proof 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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm (f * g) 1 μ < ⊤
Tactic:
. refine lt_of_le_of_lt (snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq hpq ?_ ?_) ?_
  . exact hf.aestronglyMeasurable
  . exact hg.aestronglyMeasurable
  exact ENNReal.mul_lt_top hf.snorm_ne_top hg.snorm_ne_top
Proof state after:
no goals
Theorem: memL1_Lp_mul_Lq
Proof 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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable (f * g) μ
Tactic:
exact AEStronglyMeasurable.mul hf.aestronglyMeasurable hg.aestronglyMeasurable
Proof state after:
no goals
Theorem: memL1_Lp_mul_Lq
Proof 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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm (f * g) 1 μ < ⊤
Tactic:
refine lt_of_le_of_lt (snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq hpq ?_ ?_) ?_
Proof state after:
case refine_2.refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable f μ

case refine_2.refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ

case refine_2.refine_3
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Theorem: memL1_Lp_mul_Lq
Proof state before:
case refine_2.refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable f μ

case refine_2.refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ

case refine_2.refine_3
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Tactic:
. exact hf.aestronglyMeasurable
Proof state after:
case refine_2.refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ

case refine_2.refine_3
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Theorem: memL1_Lp_mul_Lq
Proof state before:
case refine_2.refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ

case refine_2.refine_3
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Tactic:
. exact hg.aestronglyMeasurable
Proof state after:
case refine_2.refine_3
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Theorem: memL1_Lp_mul_Lq
Proof state before:
case refine_2.refine_3
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Tactic:
exact ENNReal.mul_lt_top hf.snorm_ne_top hg.snorm_ne_top
Proof state after:
no goals
Theorem: memL1_Lp_mul_Lq
Proof state before:
case refine_2.refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable f μ
Tactic:
exact hf.aestronglyMeasurable
Proof state after:
no goals
Theorem: memL1_Lp_mul_Lq
Proof state before:
case refine_2.refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ
Tactic:
exact hg.aestronglyMeasurable
Proof state after:
no goals
Theorem: integrable_Lp_mul_Lq
Proof state before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ Integrable (f * g)
Tactic:
rw [← memℒp_one_iff_integrable]
Proof state after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ Memℒp (f * g) 1
Theorem: integrable_Lp_mul_Lq
Proof state before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ Memℒp (f * g) 1
Tactic:
exact memL1_Lp_mul_Lq hpq hf hg
Proof state after:
no goals
Theorem: coeFn_L1_of_mul
Proof 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:
simp [L1_of_mul, Memℒp.coeFn_toLp]
Proof state after:
no goals
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof 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 = ξ
Proof 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‖
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof 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]
Proof 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 μ)
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof 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]
Proof 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 μ)
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof 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]
Proof 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 μ ≠ ⊤
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof 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
Proof 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 μ