Theorem: ENNReal.isConjugateExponent_toReal (ForML/LpHoelder.lean)

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

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

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

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'⟩
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)

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

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', _⟩
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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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