PhaseGrids.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.KervaireSpectral.sum_fin_val_real line 21
Source documentation
The unnormalized sum of the grid points j/d.
```
theorem sum_fin_val_real (d : ℕ) :
    (∑ j : Fin d, (j.val : ℝ)) = (d : ℝ) * ((d : ℝ)-1) / 2 := by
…
```

theorem OAI.KervaireSpectral.sum_fract_grid line 31

Source documentation

The exact fractional-part grid identity, including values on the cut.

theorem sum_fract_grid (d : ℕ) (hd : 0 < d) (x : ℝ) (hx : 0 ≤ x ∧ x < 1) :
    (∑ j : Fin d, Int.fract (x + (j.val : ℝ) / d)) =
      ((d : ℝ)-1)/2 + Int.fract ((d : ℝ)*x) := by
…

theorem OAI.KervaireSpectral.scalarRotation_nat_mul line 74
theorem OAI.KervaireSpectral.phase_pow line 82
theorem OAI.KervaireSpectral.sum_phase_grid line 90
Source documentation
The exact root-of-unity phase identity on the circle.
```
theorem sum_phase_grid {z : ℂ} (hz : ‖z‖ = 1) (d : ℕ) (hd : 0 < d) :
    (∑ j : Fin d, phase (scalarRotation ((j.val : ℝ)/d)*z)) =
      ((d : ℝ)-1)/2 + phase (z^d) := by
…
```
Mentions: OAI.KervaireSpectral.phase, OAI.KervaireSpectral.scalarRotation
theorem OAI.KervaireSpectral.sum_vectorPhase_grid line 99
Source documentation
Integrate the root-of-unity identity against a scalar spectral measure.
```
theorem sum_vectorPhase_grid (U : Operator H) (hU : U ∈ unitary (Operator H))
    (d : ℕ) (hd : 0 < d) (ξ : H) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator
theorem OAI.KervaireSpectral.sumPhase_eq_of_moments line 149
Source documentation
Positive integral moments, including mass, determine the cut-sensitive phase. This avoids assuming any Borel functional calculus naturality theorem.
```
theorem sumPhase_eq_of_moments
    (U : Operator H) (V : Operator K)
    (hU : U ∈ unitary (Operator H)) (hV : V ∈ unitary (Operator K))
    (ξ : ι → H) (η : κ → K)
    (hm : ∀ n : ℕ, vectorSum ξ (U ^ n) = vectorSum η (V ^ n)) :
    let _ := isStarNormal_of_mem_unitary hU
…
```
Mentions: OAI.KervaireSpectral.Operator, OAI.KervaireSpectral.vectorSum