pith. machine review for the scientific record. sign in
theorem proved term proof

symmetry_and_normalization_constrain_P

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 105theorem symmetry_and_normalization_constrain_P (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 106    (hSym : IsSymmetric F)
 107    (hNorm : IsNormalized F)
 108    (hCons : HasMultiplicativeConsistency F P) :
 109    ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y := by

proof body

Term-mode proof.

 110  intro y hy_pos
 111  have h := hCons 1 y one_pos hy_pos
 112  simp only [one_mul, one_div] at h
 113  rw [hNorm] at h
 114  have hSymY : F y⁻¹ = F y := (hSym y hy_pos).symm
 115  rw [hSymY] at h
 116  -- Now h : F y + F y = P 0 (F y)
 117  linarith
 118
 119/-! ## Step 2: Symmetry in Arguments Constrains P -/
 120
 121/-- If P comes from a symmetric cost function, P must be symmetric in its arguments. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.