Documentation

Lean 4 Proof

theorem uniform_onOpenSimplex (hJ : 0 < J) :
    OnOpenSimplex J (fun _ : Fin J => (1 : ℝ) / ↑J) := by
  constructor
  · intro _
    exact div_pos one_pos (Nat.cast_pos.mpr hJ)
  · rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    field_simp

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:203

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file