internlm/Lean-Github huggingface dataset:
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent (ENNReal.toReal p) (ENNReal.toReal q)

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖f x‖₊

case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
rotate_left
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent (ENNReal.toReal p) (ENNReal.toReal q)

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖f x‖₊

case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent (ENNReal.toReal p) (ENNReal.toReal q)

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖f x‖₊

case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Tactic:
. exact ENNReal.isConjugateExponent_toReal hpq hp.right hq.right
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖f x‖₊

case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖f x‖₊

case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Tactic:
. exact hf.nnnorm.aemeasurable
Proof state after:
case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊

case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Tactic:
. exact hg.nnnorm.aemeasurable
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑(((fun x => ‖f x‖₊) * fun x => ‖g x‖₊) a) ∂μ
Tactic:
simp
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑‖f a‖₊ * ↑‖g a‖₊ ∂μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ ∫⁻ (x : E), ↑‖f x * g x‖₊ ∂μ ≤ ∫⁻ (a : E), ↑‖f a‖₊ * ↑‖g a‖₊ ∂μ
Tactic:
refine lintegral_mono ?_
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ (fun x => ↑‖f x * g x‖₊) ≤ fun a => ↑‖f a‖₊ * ↑‖g a‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ (fun x => ↑‖f x * g x‖₊) ≤ fun a => ↑‖f a‖₊ * ↑‖g a‖₊
Tactic:
intro x
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
x : E
⊢ (fun x => ↑‖f x * g x‖₊) x ≤ (fun a => ↑‖f a‖₊ * ↑‖g a‖₊) x
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
x : E
⊢ (fun x => ↑‖f x * g x‖₊) x ≤ (fun a => ↑‖f a‖₊ * ↑‖g a‖₊) x
Tactic:
simp
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
x : E
⊢ ↑‖f x * g x‖₊ ≤ ↑‖f x‖₊ * ↑‖g x‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
x : E
⊢ ↑‖f x * g x‖₊ ≤ ↑‖f x‖₊ * ↑‖g x‖₊
Tactic:
norm_cast
Proof state after:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
x : E
⊢ ‖f x * g x‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
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_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case hp'
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ p ≠ 0
Tactic:
refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
Proof state after:
case hp'
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ 1 ≤ p
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case hp'
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ 1 ≤ p
Tactic:
exact ENNReal.one_le_of_conjugate hpq
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case hq'
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ q ≠ 0
Tactic:
refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
Proof state after:
case hq'
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ 1 ≤ q
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case hq'
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ 1 ≤ q
Tactic:
exact ENNReal.one_le_of_conjugate' hpq
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent (ENNReal.toReal p) (ENNReal.toReal q)
Tactic:
exact ENNReal.isConjugateExponent_toReal hpq hp.right hq.right
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.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 : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖f x‖₊
Tactic:
exact hf.nnnorm.aemeasurable
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inl.intro.refine_4
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
exact hg.nnnorm.aemeasurable
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq : p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
cases hpq with
| inl hpq =>
  simp [hpq.left, hpq.right, -snorm_exponent_top] at *
  refine snorm_le_snorm_mul_snorm_top 1 hf g (fun u v => u * v) ?_
  refine Filter.eventually_of_forall ?_
  intro x
  simp
  exact nnnorm_mul_le (f x) (g x)
| inr hpq =>
  simp [hpq.left, hpq.right, -snorm_exponent_top] at *
  refine snorm_le_snorm_top_mul_snorm 1 f hg (fun u v => u * v) ?_
  refine Filter.eventually_of_forall ?_
  intro x
  simp
  exact nnnorm_mul_le (f x) (g x)
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inl
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq : p = 1 ∧ q = ⊤
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
simp [hpq.left, hpq.right, -snorm_exponent_top] at *
Proof state after:
case inr.inl
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
⊢ snorm (f * g) 1 μ ≤ snorm f 1 μ * snorm g ⊤ μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inl
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
⊢ snorm (f * g) 1 μ ≤ snorm f 1 μ * snorm g ⊤ μ
Tactic:
refine snorm_le_snorm_mul_snorm_top 1 hf g (fun u v => u * v) ?_
Proof state after:
case inr.inl
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) ∂μ, ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inl
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) ∂μ, ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
refine Filter.eventually_of_forall ?_
Proof state after:
case inr.inl
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), ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inl
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), ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
intro x
Proof state after:
case inr.inl
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
⊢ ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inl
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
⊢ ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
simp
Proof state after:
case inr.inl
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‖₊
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof state before:
case inr.inl
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_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∞
hpq✝ : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq : p = ⊤ ∧ q = 1
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
simp [hpq.left, hpq.right, -snorm_exponent_top] at *
Proof state after:
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
⊢ snorm (f * g) 1 μ ≤ snorm f ⊤ μ * snorm g 1 μ
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
⊢ snorm (f * g) 1 μ ≤ snorm f ⊤ μ * snorm g 1 μ
Tactic:
refine snorm_le_snorm_top_mul_snorm 1 f hg (fun u v => u * v) ?_
Proof state after:
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) ∂μ, ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
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) ∂μ, ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
refine Filter.eventually_of_forall ?_
Proof state after:
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), ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
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), ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
intro x
Proof state after:
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
⊢ ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
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
⊢ ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
Tactic:
simp
Proof state after:
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‖₊