Theorem: snorm_mul_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✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
cases ENNReal.conjugate_cases hpq with
| inl hpq =>
  rcases hpq with ⟨hp, hq⟩
  have hp' : p ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact ENNReal.one_le_of_conjugate hpq
  have hq' : q ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact ENNReal.one_le_of_conjugate' hpq
  rw [snorm_eq_lintegral_rpow_nnnorm hp' hp.right]
  rw [snorm_eq_lintegral_rpow_nnnorm hq' hq.right]
  rw [snorm_one_eq_lintegral_nnnorm]
  simp [-one_div]
  refine le_trans ?_ (NNReal.lintegral_mul_le_Lp_mul_Lq ?_ ?_ ?_)
  rotate_left
  . exact ENNReal.isConjugateExponent_toReal hpq hp.right hq.right
  . exact hf.nnnorm.aemeasurable
  . exact hg.nnnorm.aemeasurable
  simp
  refine lintegral_mono ?_
  intro x
  simp
  norm_cast
  exact nnnorm_mul_le (f x) (g x)
| inr hpq =>
  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)
State after:
no goals

State before:
case 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 : (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
rcases hpq with ⟨hp, hq⟩
State after:
case inl.intro
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 ≠ ⊤
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ

State before:
case inl.intro
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 ≠ ⊤
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
have hp' : p ≠ 0
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 ≠ ⊤
⊢ p ≠ 0

case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ

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

case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
. refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
  exact ENNReal.one_le_of_conjugate hpq
State after:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ

State before:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
have hq' : q ≠ 0
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
⊢ q ≠ 0

case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ

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

case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
. refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
  exact ENNReal.one_le_of_conjugate' hpq
State after:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ

State before:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
Tactic:
rw [snorm_eq_lintegral_rpow_nnnorm hp' hp.right]
State after:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) * snorm g q μ

State before:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤ (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) * snorm g q μ
Tactic:
rw [snorm_eq_lintegral_rpow_nnnorm hq' hq.right]
State after:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)

State before:
case inl.intro
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
⊢ snorm (f * g) 1 μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)
Tactic:
rw [snorm_one_eq_lintegral_nnnorm]
State after:
case inl.intro
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 * g) x‖₊ ∂μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)

State before:
case inl.intro
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 * g) x‖₊ ∂μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)
Tactic:
simp [-one_div]
State after:
case inl.intro
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‖₊ ∂μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)

State before:
case inl.intro
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‖₊ ∂μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)
Tactic:
refine le_trans ?_ (NNReal.lintegral_mul_le_Lp_mul_Lq ?_ ?_ ?_)
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) ∂μ

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

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

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

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

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

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
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‖₊ ∂μ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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