Documentation

Lean 4 Proof

theorem cesPotential_affine_in_T (_hJ : 0 < J) (q : ℝ) (p ε : Fin J → ℝ)
    (T₁ T₂ α : ℝ) (_hα : 0 ≤ α) (_hα1 : α ≤ 1) :
    cesPotential J q (α * T₁ + (1 - α) * T₂) p ε =
    α * cesPotential J q T₁ p ε + (1 - α) * cesPotential J q T₂ p ε := by
  simp only [cesPotential]
  ring

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:91

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file