OAI/Combinatorics/SphericalRamsey/CopyInvariant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GrahamSpherical.weighted_copy_derivation_energy line 11

   Source documentation

   All distance-preserving copies, with no affine-form or dimension premise.

   theorem weighted_copy_derivation_energy {n : ℕ}
       (D : Derivation ℤ ℝ ℝ)
       (hD : D parameter = (1 + parameter ^ 2) / 2)
       (f : witness → Point n) (hf : Isometry f) :
       ∑ i : Label, (weight i : ℝ) *
         derivationEnergy D (f ⟨vertex i, ⟨i, rfl⟩⟩) = 8 := by
   …

   Mentions: OAI.GrahamSpherical.parameter, OAI.GrahamSpherical.witness, OAI.GrahamSpherical.Point, OAI.GrahamSpherical.Label, OAI.GrahamSpherical.weight, OAI.GrahamSpherical.derivationEnergy, OAI.GrahamSpherical.vertex

2. theorem OAI.GrahamSpherical.derivationColor_avoids line 36