internlm/Lean-Github huggingface dataset:
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
cases conjugate_cases hpq with
| inr hpq =>
  simp at *
  cases hpq with
  | inl hpq => rcases hpq with ⟨_, hq'⟩; contradiction
  | inr hpq => rcases hpq with ⟨hp', _⟩; contradiction
| inl hpq =>
  rcases hpq with ⟨hp, hq⟩
  have hp' : p ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact one_le_of_conjugate hpq
  have hq' : q ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact one_le_of_conjugate' hpq
  cases p with | none => contradiction | some p =>
  cases q with | none => contradiction | some q =>
  simp at *
  constructor
  . norm_cast
  . rw [← ENNReal.coe_inv hp', ← ENNReal.coe_inv hq'] at hpq
    norm_cast at hpq
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inr
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
hpq : p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
simp at *
Proof state after:
case inr
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hpq : p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inr
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hpq : p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Tactic:
cases hpq with
| inl hpq => rcases hpq with ⟨_, hq'⟩; contradiction
| inr hpq => rcases hpq with ⟨hp', _⟩; contradiction
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inr.inl
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hpq : p = 1 ∧ q = ⊤
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Tactic:
rcases hpq with ⟨_, hq'⟩
Proof state after:
case inr.inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
left✝ : p = 1
hq' : q = ⊤
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inr.inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
left✝ : p = 1
hq' : q = ⊤
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Tactic:
contradiction
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inr.inr
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hpq : p = ⊤ ∧ q = 1
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Tactic:
rcases hpq with ⟨hp', _⟩
Proof state after:
case inr.inr.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hp' : p = ⊤
right✝ : q = 1
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inr.inr.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp : ¬p = ⊤
hq : ¬q = ⊤
hp' : p = ⊤
right✝ : q = 1
⊢ (ENNReal.toNNReal p).IsConjExponent (ENNReal.toNNReal q)
Tactic:
contradiction
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
hp : p ≠ ⊤
hq : q ≠ ⊤
hpq : (1 < p ∧ p ≠ ⊤) ∧ 1 < q ∧ q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
rcases hpq with ⟨hp, hq⟩
Proof state after:
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
have hp' : p ≠ 0
Proof state after:
case hp'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ p ≠ 0

case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case hp'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ p ≠ 0

case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
. refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
  exact one_le_of_conjugate hpq
Proof state after:
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
have hq' : q ≠ 0
Proof state after:
case hq'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ q ≠ 0

case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case hq'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ q ≠ 0

case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
. refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
  exact one_le_of_conjugate' hpq
Proof state after:
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal p) ↑(ENNReal.toNNReal q)
Tactic:
cases p with | none => contradiction | some p =>
cases q with | none => contradiction | some q =>
simp at *
constructor
. norm_cast
. rw [← ENNReal.coe_inv hp', ← ENNReal.coe_inv hq'] at hpq
  norm_cast at hpq
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case hp'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
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'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ 1 ≤ p
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case hp'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
⊢ 1 ≤ p
Tactic:
exact one_le_of_conjugate hpq
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case hq'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
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'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ 1 ≤ q
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case hq'
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
hp✝ : p ≠ ⊤
hq✝ : q ≠ ⊤
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
⊢ 1 ≤ q
Tactic:
exact one_le_of_conjugate' hpq
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.none
q : ℝ≥0∞
hq✝ : q ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hq' : q ≠ 0
hpq : none⁻¹ + q⁻¹ = 1
hp✝ : none ≠ ⊤
hp : 1 < none ∧ none ≠ ⊤
hp' : none ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal none) ↑(ENNReal.toNNReal q)
Tactic:
contradiction
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some
q : ℝ≥0∞
hq✝ : q ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hq' : q ≠ 0
p : ℝ≥0
hpq : (some p)⁻¹ + q⁻¹ = 1
hp✝ : some p ≠ ⊤
hp : 1 < some p ∧ some p ≠ ⊤
hp' : some p ≠ 0
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal (some p)) ↑(ENNReal.toNNReal q)
Tactic:
cases q with | none => contradiction | some q =>
simp at *
constructor
. norm_cast
. rw [← ENNReal.coe_inv hp', ← ENNReal.coe_inv hq'] at hpq
  norm_cast at hpq
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.none
p : ℝ≥0
hp✝ : some p ≠ ⊤
hp : 1 < some p ∧ some p ≠ ⊤
hp' : some p ≠ 0
hq✝ : none ≠ ⊤
hq : 1 < none ∧ none ≠ ⊤
hq' : none ≠ 0
hpq : (some p)⁻¹ + none⁻¹ = 1
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal (some p)) ↑(ENNReal.toNNReal none)
Tactic:
contradiction
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some
p : ℝ≥0
hp✝ : some p ≠ ⊤
hp : 1 < some p ∧ some p ≠ ⊤
hp' : some p ≠ 0
q : ℝ≥0
hq✝ : some q ≠ ⊤
hq : 1 < some q ∧ some q ≠ ⊤
hq' : some q ≠ 0
hpq : (some p)⁻¹ + (some q)⁻¹ = 1
⊢ Real.IsConjExponent ↑(ENNReal.toNNReal (some p)) ↑(ENNReal.toNNReal (some q))
Tactic:
simp at *
Proof state after:
case inl.intro.some.some
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p.IsConjExponent q
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p.IsConjExponent q
Tactic:
constructor
Proof state after:
case inl.intro.some.some.one_lt
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ 1 < p

case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some.one_lt
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ 1 < p

case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Tactic:
. norm_cast
Proof state after:
case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Tactic:
. rw [← ENNReal.coe_inv hp', ← ENNReal.coe_inv hq'] at hpq
  norm_cast at hpq
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some.one_lt
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ 1 < p
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Tactic:
rw [← ENNReal.coe_inv hp', ← ENNReal.coe_inv hq'] at hpq
Proof state after:
case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : ↑p⁻¹ + ↑q⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Theorem: ENNReal.isConjugateExponent_toReal
Proof state before:
case inl.intro.some.some.inv_add_inv_conj
p q : ℝ≥0
hpq : ↑p⁻¹ + ↑q⁻¹ = 1
hp✝ : True
hp : 1 < p
hp' : ¬p = 0
hq✝ : True
hq : 1 < q
hq' : ¬q = 0
⊢ p⁻¹ + q⁻¹ = 1
Tactic:
norm_cast at hpq
Proof state after:
no goals
Theorem: snorm_mul_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✝ : 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)
Proof state after:
no goals
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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⟩
Proof 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 μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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
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 ≠ ⊤
⊢ 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 μ
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

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
Proof 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 μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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
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
⊢ 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 μ
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

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
Proof 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 μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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]
Proof 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 μ
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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]
Proof 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)
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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]
Proof 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)
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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]
Proof 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)
Theorem: snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq
Proof 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 ?_ ?_ ?_)
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) ∂μ

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