ModelGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Geometric consequences of the actual cyclic representative system.

theorem OAI.QuantitativeVanDerWaerden.yRep_step_lattice line 10
Source documentation
The coordinate lattice is unchanged when a real step is shifted by an integer.
```
theorem yRep_step_lattice {q D dilation : ℕ} (hq : 0 < q)
    (d : CyclicGroup q D) (i : Fin D) {w : ℝ}
    (hstep : ∃ z : ℤ, yRep q D dilation d i - w = z) :
    ∃ z : ℤ, (q : ℝ) ^ (i.val + 1) * w = z := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.yRep
theorem OAI.QuantitativeVanDerWaerden.yRep_step_abs_lower line 21
Source documentation
Every nonzero lifted coordinate step is at least one coordinate lattice unit.
```
theorem yRep_step_abs_lower {q D dilation : ℕ} (hq : 0 < q)
    (d : CyclicGroup q D) (i : Fin D) {w : ℝ}
    (hstep : ∃ z : ℤ, yRep q D dilation d i - w = z) (hw : w ≠ 0) :
    1 / (q : ℝ) ^ (i.val + 1) ≤ |w| := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.yRep

theorem OAI.QuantitativeVanDerWaerden.yRep_step_mesh_lower line 30

Source documentation

The mesh cutoff q^(-(D+1)) lies below every nonzero lifted step.

theorem yRep_step_mesh_lower {q D dilation : ℕ} (hq : 0 < q)
    (d : CyclicGroup q D) (i : Fin D) {w : ℝ}
    (hstep : ∃ z : ℤ, yRep q D dilation d i - w = z) (hw : w ≠ 0) :
    1 / (q : ℝ) ^ (D + 1) ≤ 1 / (q : ℝ) ^ D ∧
      1 / (q : ℝ) ^ D ≤ |w| := by
…

Mentions: OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.yRep