awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
⊢ Eq (α := Fin (Fintype.card n) → ℝ) hA.eigenvalues₀ hB.eigenvalues₀
have mpr : List.ofFn (n := Fintype.card n) hA.eigenvalues₀ = List.ofFn (n := Fintype.card n) hB.eigenvalues₀
Tactic: simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
mpr : List.ofFn (n := Fintype.card n) hA.eigenvalues₀ = List.ofFn (n := Fintype.card n) hB.eigenvalues₀
⊢ Eq (α := Fin (Fintype.card n) → ℝ) hA.eigenvalues₀ hB.eigenvalues₀
have mpr₁ : Eq (α := List ℝ)
  (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) (Polynomial.roots A.charpoly)) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
  (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) (Polynomial.roots B.charpoly)) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
Tactic: simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
| A.rank
have rw : ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues) *
    (↑(star hA.eigenvectorUnitary) : Matrix n n 𝕜)).rank
Tactic: rw [hA.spectral_theorem, conjStarAlgAut_apply, ← coe_star]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ A.rank = (diagonal hA.eigenvalues).rank
have conv_lhs : ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues) *
      (↑(star hA.eigenvectorUnitary) : Matrix n n 𝕜)).rank =
  (diagonal hA.eigenvalues).rank
Tactic: conv_lhs => rw [hA.spectral_theorem, conjStarAlgAut_apply, ← coe_star]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ A.rank = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
have rw : (diagonal hA.eigenvalues).rank = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
Tactic: rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw : (diagonal hA.eigenvalues).rank = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
⊢ A.rank = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
have rw₁ : Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 } = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
Tactic: rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : 𝕜
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : 𝕜
⊢ x ∈ spectrum 𝕜 A ↔ Membership.mem (γ := Set 𝕜) (RCLike.ofReal '' Set.range hA.eigenvalues) x
have conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: conv_lhs => rw [hA.spectral_theorem]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : ℝ
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [hA.spectral_theorem, ← spectrum.algebraMap_mem_iff 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : ℝ
⊢ x ∈ spectrum ℝ A ↔ x ∈ Set.range hA.eigenvalues
have conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: conv_lhs => rw [hA.spectral_theorem, ← spectrum.algebraMap_mem_iff 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
h : A = 0
⊢ hA.eigenvalues = 0
have h₁ : ∀ (x : n), hA.eigenvalues x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ hA.eigenvalues = 0 ↔ A = 0
have refine : ∀ (h : hA.eigenvalues = 0), A = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by ext; simp [h, eigenvalues_eq]⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ hA.eigenvalues ≠ 0
have contrapose : ∀ (h_ne : hA.eigenvalues = 0), A = 0
Tactic: contrapose h_ne
Cleared hypotheses: h_ne
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
⊢ A = 0
have this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: have := hA.spectral_theorem
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have this : hA.eigenvalues ≠ 0
Tactic: have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have obtain : ∀ (i : n) (hi : hA.eigenvalues i ≠ 0 i), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
Tactic: obtain ⟨i, hi⟩ := Function.ne_iff.mp this
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have have : hA.eigenvalues ≠ 0
Tactic: classical
  have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
  obtain ⟨i, hi⟩ := Function.ne_iff.mp this
  exact ⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
have : hA.eigenvalues ≠ 0
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have have₁ : ∀ (this : hA.eigenvalues ≠ 0), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
Tactic: classical
  have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
  obtain ⟨i, hi⟩ := Function.ne_iff.mp this
  exact ⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
have : hA.eigenvalues ≠ 0
have₁ : ∀ (this : hA.eigenvalues ≠ 0), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have₂ : hA.eigenvalues ≠ 0
have₃ have₄ : ∀ (this : hA.eigenvalues ≠ 0), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have have₅ : ∀ (this : hA.eigenvalues ≠ 0) (i : n) (hi : hA.eigenvalues i ≠ 0 i),
  ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
Tactic: classical
  have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
  obtain ⟨i, hi⟩ := Function.ne_iff.mp this
  exact ⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have pos : ∀ (A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
Tactic: by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
pos : ∀ (A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have neg : ∀ (A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
Tactic: by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have pos : ∀ (i : ι) (his : i ∈ s) (hzi : z i = 0) (hwi : w i ≠ 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
Tactic: rcases A with ⟨i, his, hzi, hwi⟩
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have pos : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)
Tactic: rw [prod_eq_zero his]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
pos : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have pos₁ : z i ^ w i = 0
Tactic: rw [prod_eq_zero his]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
have pos : HPow.hPow (α := ℝ) 0 (w i) = 0
Tactic: rw [hzi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have this : rexp (∑ i ∈ s, w i • log (z i)) ≤ ∑ i ∈ s, w i • rexp (log (z i))
Tactic: have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : rexp (∑ i ∈ s, w i • log (z i)) ≤ ∑ i ∈ s, w i • rexp (log (z i))
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have this₁ : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
Tactic: simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have h : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
have h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
Tactic: apply prod_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))
have h : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
Tactic: convert! this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have h₁ : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
Tactic: convert! this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
⊢ z i ^ w i = rexp (log (z i) * w i)
have h : ∀ (hz : 0 = z i), z i ^ w i = rexp (log (z i) * w i)
Tactic: rcases eq_or_lt_of_le (hz i hi) with hz | hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
h : ∀ (hz : 0 = z i), z i ^ w i = rexp (log (z i) * w i)
⊢ z i ^ w i = rexp (log (z i) * w i)
have h₁ : ∀ (hz : 0 < z i), z i ^ w i = rexp (log (z i) * w i)
Tactic: rcases eq_or_lt_of_le (hz i hi) with hz | hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
⊢ w i * z i = w i * rexp (log (z i))
have h : ∀ (hz : 0 = z i), w i * z i = w i * rexp (log (z i))
Tactic: rcases eq_or_lt_of_le (hz i hi) with hz | hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
h : ∀ (hz : 0 = z i), w i * z i = w i * rexp (log (z i))
⊢ w i * z i = w i * rexp (log (z i))
have h₁ : ∀ (hz : 0 < z i), w i * z i = w i * rexp (log (z i))
Tactic: rcases eq_or_lt_of_le (hz i hi) with hz | hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz_1 : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * rexp (log (z i))
have h : w i * z i = w i * z i
Tactic: rw [exp_log hz]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)
have h : HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
Tactic: convert! geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz using 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)
have h₁ : HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
Tactic: convert! geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz using 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
h₁ : HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)
have convert_1 : ∀ i ∈ s, LE.le (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)
Tactic: convert! geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz using 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
h₁ : HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
convert_1 : ∀ i ∈ s, LE.le (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)
have convert_2 : Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1
Tactic: convert! geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz using 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
have h : Eq (α := ℝ) (∏ i ∈ s, HPow.hPow (β := ℝ) (z i ^ w i) (∑ i ∈ s, w i)⁻¹) (∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i))
Tactic: rw [← finsetProd_rpow _ _ (fun i hi => rpow_nonneg (hz _ hi) _) _]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ Eq (α := ℝ) (∏ i ∈ s, HPow.hPow (β := ℝ) (z i ^ w i) (∑ i ∈ s, w i)⁻¹) (∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i))
have h : ∀ (x : ι) (ih : x ∈ s), HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x / ∑ i ∈ s, w i)
Tactic: refine Finset.prod_congr rfl (fun _ ih => ?_)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
x : ι
ih : x ∈ s
⊢ HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x / ∑ i ∈ s, w i)
have h : HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x * (∑ i ∈ s, w i)⁻¹)
Tactic: rw [div_eq_mul_inv, rpow_mul (hz _ ih)]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
x : ι
ih : x ∈ s
h : HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x * (∑ i ∈ s, w i)⁻¹)
⊢ HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x / ∑ i ∈ s, w i)
have h₁ : HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹
Tactic: rw [div_eq_mul_inv, rpow_mul (hz _ ih)]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
have h : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
have h₁ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * ((∑ i ∈ s, w i)⁻¹ * z x)
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]