Theorem: memL1_Lp_smul_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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ Memℒp (f • g) 1
Tactic:
refine And.intro ?_ ?_
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 : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm (f • g) 1 μ < ⊤

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 : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm (f • g) 1 μ < ⊤
Tactic:
. exact AEStronglyMeasurable.smul hf.aestronglyMeasurable hg.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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm (f • g) 1 μ < ⊤

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 : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm (f • g) 1 μ < ⊤
Tactic:
. refine lt_of_le_of_lt (snorm_smul_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
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ AEStronglyMeasurable (f • g) μ
Tactic:
exact AEStronglyMeasurable.smul hf.aestronglyMeasurable hg.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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm (f • g) 1 μ < ⊤
Tactic:
refine lt_of_le_of_lt (snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq hpq ?_ ?_) ?_
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤

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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Tactic:
. exact hf.aestronglyMeasurable
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤

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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤
Tactic:
. exact hg.aestronglyMeasurable
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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm f p μ * snorm g q μ < ⊤

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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
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
State after:
no goals

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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ AEStronglyMeasurable f μ
Tactic:
exact hf.aestronglyMeasurable
State after:
no goals

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✝³ : NormedAddCommGroup 𝕜
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : SMulZeroClass 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ
Tactic:
exact hg.aestronglyMeasurable
State after:
no goals