Documentation

Lean 4 Proof

theorem euler_identity_at_uniform (hJ : 0 < J) (ε₀ : ℝ) :
    ∑ _j : Fin J, ε₀ * ((1 : ℝ) / ↑J) = ε₀ := by
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:212

Module Section

Theorems 5-7, Corollaries 2-4, Propositions 8-11:

In the same file