Theorem: memL1_Lp_mul_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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
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✝ : 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 μ < ⊤

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
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 μ < ⊤

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
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 : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable (f * g) μ
Tactic:
exact AEStronglyMeasurable.mul 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✝ : 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 ?_ ?_) ?_
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 μ < ⊤

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
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 μ < ⊤

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
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 μ < ⊤

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
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✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
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✝ : NormedRing 𝕜
f : E → 𝕜
hf : Memℒp f p
g : E → 𝕜
hg : Memℒp g q
⊢ AEStronglyMeasurable g μ
Tactic:
exact hg.aestronglyMeasurable
State after:
no goals