Theorem: snorm_smul_L1_le_snorm_Lp_mul_snorm_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 : 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 μ
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 μ

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

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

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 ?_
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‖‖

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
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‖

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
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‖

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)
State after:
no goals

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

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 ?_
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 μ

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
State after:
no goals