OAI/Combinatorics/SphericalRamsey/EnergyIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GrahamSpherical.rotation_norm_sq line 12
2. theorem OAI.GrahamSpherical.derivation_u_v line 18
3. theorem OAI.GrahamSpherical.weighted_coordinate_square line 24

   Source documentation

   The translation and orientation-derivative coefficients are arbitrary.

   theorem weighted_coordinate_square (D : Derivation ℤ ℝ ℝ)
       (hD : D parameter = (1 + parameter ^ 2) / 2)
       (p a b c d : ℝ) :
       ∑ i : Label, (weight i : ℝ) *
         (p + a * coordinates i 0 + b * coordinates i 1 +
           c * D (coordinates i 0) + d * D (coordinates i 1)) ^ 2 =
           4 * (c ^ 2 + d ^ 2) := by
   …

   Mentions: OAI.GrahamSpherical.parameter, OAI.GrahamSpherical.Label, OAI.GrahamSpherical.weight, OAI.GrahamSpherical.coordinates

4. theorem OAI.GrahamSpherical.weighted_affine_derivation_energy line 42

   Source documentation

   Weighted derivative energy for an actual affine placement. The mixed orthogonality condition is not needed after the exact moment cancellation.

   theorem weighted_affine_derivation_energy {n : ℕ}
       (D : Derivation ℤ ℝ ℝ)
       (hD : D parameter = (1 + parameter ^ 2) / 2)
       (z A B : Fin n → ℝ)
       (hA : ∑ j, A j ^ 2 = 1) (hB : ∑ j, B j ^ 2 = 1) :
       ∑ i : Label, (weight i : ℝ) * ∑ j : Fin n,
         (D (z j + coordinates i 0 * A j + coordinates i 1 * B j)) ^ 2 = 8 := by
   …

   Mentions: OAI.GrahamSpherical.parameter, OAI.GrahamSpherical.Label, OAI.GrahamSpherical.weight, OAI.GrahamSpherical.coordinates