internlm/Lean-Github huggingface dataset:
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inr
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq✝ hpq : True
x : E
⊢ ‖f x * g x‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
exact nnnorm_mul_le (f x) (g x)
Proof state after:
no goals
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (f • g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
suffices : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (f • g) 1 μ ≤ snorm f p μ * snorm g q μ

case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (f • g) 1 μ ≤ snorm f p μ * snorm g q μ

case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
Tactic:
. rw [← snorm_norm (f • g), ← snorm_norm f, ← snorm_norm g]
  refine le_trans this ?_
  exact snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq hpq hf.norm hg.norm
Proof state after:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
Tactic:
simp
Proof state after:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => f x • g x) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ snorm (fun x => f x • g x) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
Tactic:
refine snorm_mono ?_
Proof state after:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ ∀ (x : E), ‖f x • g x‖ ≤ ‖‖f x‖ * ‖g x‖‖
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ ∀ (x : E), ‖f x • g x‖ ≤ ‖‖f x‖ * ‖g x‖‖
Tactic:
simp
Proof state after:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ ∀ (x : E), ‖f x • g x‖ ≤ ‖f x‖ * ‖g x‖
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
⊢ ∀ (x : E), ‖f x • g x‖ ≤ ‖f x‖ * ‖g x‖
Tactic:
intro x
Proof state after:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
x : E
⊢ ‖f x • g x‖ ≤ ‖f x‖ * ‖g x‖
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case this
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 : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
x : E
⊢ ‖f x • g x‖ ≤ ‖f x‖ * ‖g x‖
Tactic:
exact norm_smul_le (f x) (g x)
Proof state after:
no goals
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (f • g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
rw [← snorm_norm (f • g), ← snorm_norm f, ← snorm_norm g]
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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (fun x => ‖(f • g) x‖) 1 μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) q μ
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (fun x => ‖(f • g) x‖) 1 μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) q μ
Tactic:
refine le_trans this ?_
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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) q μ
Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_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 : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → F
hg : AEStronglyMeasurable g μ
this : snorm (fun x => ‖f x • g x‖) 1 μ ≤ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ
⊢ snorm (fun x => ‖f x‖ * ‖g x‖) 1 μ ≤ snorm (fun x => ‖f x‖) p μ * snorm (fun x => ‖g x‖) q μ
Tactic:
exact snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq hpq hf.norm hg.norm
Proof state after:
no goals
Theorem: memL1_Lp_smul_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 : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : 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 μ < ⊤
Theorem: memL1_Lp_smul_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 : 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
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 : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ snorm (f • g) 1 μ < ⊤
Theorem: memL1_Lp_smul_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 : 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
Proof state after:
no goals
Theorem: memL1_Lp_smul_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 : 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
Proof state after:
no goals
Theorem: memL1_Lp_smul_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 : 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 ?_ ?_) ?_
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✝³ : 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 μ < ⊤
Theorem: memL1_Lp_smul_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✝³ : 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
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✝³ : 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 μ < ⊤
Theorem: memL1_Lp_smul_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✝³ : 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
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✝³ : 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 μ < ⊤
Theorem: memL1_Lp_smul_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✝³ : 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
Proof state after:
no goals
Theorem: memL1_Lp_smul_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✝³ : 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
Proof state after:
no goals
Theorem: memL1_Lp_smul_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✝³ : 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
Proof state after:
no goals
Theorem: integrable_Lp_smul_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 : E → 𝕜
hf : Memℒp f p
g : E → F
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✝³ : 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
Theorem: integrable_Lp_smul_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 : E → 𝕜
hf : Memℒp f p
g : E → F
hg : Memℒp g q
⊢ Memℒp (f • g) 1
Tactic:
exact memL1_Lp_smul_Lq hpq hf hg
Proof state after:
no goals
Theorem: coeFn_L1_of_Lp_smul_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)
⊢ ↑↑(L1_of_Lp_smul_Lq hpq f g) =ᵐ[μ] ↑↑f • ↑↑g
Tactic:
simp [L1_of_Lp_smul_Lq, Memℒp.coeFn_toLp]
Proof state after:
no goals
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)
⊢ ‖L1_of_Lp_smul_Lq hpq f g‖ ≤ ‖f‖ * ‖g‖
Tactic:
generalize hξ : L1_of_Lp_smul_Lq 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✝³ : 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 = ξ
⊢ ‖ξ‖ ≤ ‖f‖ * ‖g‖
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 = ξ
⊢ ‖ξ‖ ≤ ‖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✝³ : 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 = ξ
⊢ ENNReal.toReal (snorm (↑↑ξ) 1 μ) ≤ ENNReal.toReal (snorm (↑↑f) p μ) * ENNReal.toReal (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 = ξ
⊢ 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✝³ : 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 = ξ
⊢ ENNReal.toReal (snorm (↑↑ξ) 1 μ) ≤ ENNReal.toReal (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 = ξ
⊢ 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✝³ : 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 μ ≠ ⊤