PhaseEncoding.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EuclideanFiveColor.PhaseEncoding.phases line 23
def OAI.EuclideanFiveColor.PhaseEncoding.elem line 26
def OAI.EuclideanFiveColor.PhaseEncoding.encoding line 29
Source documentation
Exactly the elementary symmetric functions of degrees 1,…,m.
```
def encoding {m : ℕ} (z : Fin m → Circle) : Fin m → ℂ :=
…
```
def OAI.EuclideanFiveColor.PhaseEncoding.phasePolynomial line 32
theorem OAI.EuclideanFiveColor.PhaseEncoding.card_phases line 35
theorem OAI.EuclideanFiveColor.PhaseEncoding.elem_zero line 38
theorem OAI.EuclideanFiveColor.PhaseEncoding.elem_eq_sum line 41
theorem OAI.EuclideanFiveColor.PhaseEncoding.continuous_encoding line 46
theorem OAI.EuclideanFiveColor.PhaseEncoding.polynomial_expansion line 52
theorem OAI.EuclideanFiveColor.PhaseEncoding.eval_at_phase line 61
theorem OAI.EuclideanFiveColor.PhaseEncoding.eval_expansion line 67
theorem OAI.EuclideanFiveColor.PhaseEncoding.eval_difference line 75
theorem OAI.EuclideanFiveColor.PhaseEncoding.eval_difference_bound line 87
Source documentation
A coefficient bound on the unit circle, with the common leading term removed.
```
theorem eval_difference_bound {m : ℕ} (z w : Fin m → Circle) (a : Circle) :
    ‖(phasePolynomial w).eval (a : ℂ) - (phasePolynomial z).eval (a : ℂ)‖ ≤
      m * dist (encoding z) (encoding w) := by
…
```
Mentions: OAI.EuclideanFiveColor.PhaseEncoding.phasePolynomial, OAI.EuclideanFiveColor.PhaseEncoding.encoding

theorem OAI.EuclideanFiveColor.PhaseEncoding.close_encoding_each_phase line 105

Source documentation

An explicit uniform inverse estimate sufficient for the phase collision step.

theorem close_encoding_each_phase {m : ℕ} (hm : 0 < m)
    (z w : Fin m → Circle) {ρ : ℝ} (hρ : 0 < ρ)
    (hzw : dist (encoding z) (encoding w) < ρ ^ m / m) :
    ∀ i, ∃ j, dist (z i : ℂ) (w j : ℂ) < ρ := by
…

Mentions: OAI.EuclideanFiveColor.PhaseEncoding.encoding

def OAI.EuclideanFiveColor.PhaseEncoding.fromPowers line 130
Source documentation
Newton reconstruction from the entire sequence of power sums.
```
def fromPowers (p : ℕ → ℂ) (n : ℕ) : ℂ :=
…
```
lemma OAI.EuclideanFiveColor.PhaseEncoding.measurable_fromPowers line 139
lemma OAI.EuclideanFiveColor.PhaseEncoding.newton_elem line 153
lemma OAI.EuclideanFiveColor.PhaseEncoding.filtered_antidiagonal_sum line 163
theorem OAI.EuclideanFiveColor.PhaseEncoding.fromPowers_eq_elem line 173
def OAI.EuclideanFiveColor.PhaseEncoding.kernelEncoding line 204
Source documentation
The measurable phase encoding, defined without a measurable enumeration.
```
def kernelEncoding (β : Kernel Y G) (χ : G → ℂ) (m : ℕ) (y : Y) : Fin m → ℂ :=
…
```
theorem OAI.EuclideanFiveColor.PhaseEncoding.measurable_kernelEncoding line 207
theorem OAI.EuclideanFiveColor.PhaseEncoding.moments_uniform_list line 216
theorem OAI.EuclideanFiveColor.PhaseEncoding.kernelEncoding_eq_encoding line 231
Source documentation
On every uniform finite fiber, the formula is exactly the source's elementary-symmetric vector, including repetitions of equal phases.
```
theorem kernelEncoding_eq_encoding [MeasurableSingletonClass G] (β : Kernel Y G) (χ : G → Circle)
    (m : ℕ) (hm : 0 < m) (y : Y) (g : Fin m → G)
    (hβ : β y = (m : ℝ≥0∞)⁻¹ • ∑ i, Measure.dirac (g i)) :
    kernelEncoding β (fun d => (χ d : ℂ)) m y = encoding (fun i => χ (g i)) := by
…
```
Mentions: OAI.EuclideanFiveColor.PhaseEncoding.kernelEncoding, OAI.EuclideanFiveColor.PhaseEncoding.encoding
theorem OAI.EuclideanFiveColor.PhaseEncoding.exists_encoding_bound line 247
Source documentation
Boundedness of the exact phase encoding, from compactness of the phase torus.
```
theorem exists_encoding_bound (m : ℕ) :
    ∃ B : ℝ, ∀ z : Fin m → Circle, ‖encoding z‖ ≤ B := by
…
```
Mentions: OAI.EuclideanFiveColor.PhaseEncoding.encoding