HaarPrefixCoordinates.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Product Haar measure in increment and endpoint coordinates

The change (u₁, …, uₕ) ↦ (u₁, u₁u₂, …, u₁⋯uₕ) preserves product Haar measure. Its inverse is the successive-difference map used in the endpoint-tuple volume argument.

def OAI.PolycyclicRecognition.prefixShear line 20

def OAI.PolycyclicRecognition.prefixCoordinateEquiv line 32

Source documentation

Finite multiplication in successive endpoint coordinates, retaining the first coordinate as the first increment.

def prefixCoordinateEquiv : (n : ℕ) → (Fin n → G) ≃ᵐ (Fin n → G)
  | 0 => MeasurableEquiv.refl _
  | n + 1 =>
    let split := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) => G) 0
…

theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_zero line 39
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_succ line 44
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_increment line 50
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_symm_increment line 63
Source documentation
The inverse records the first point and the consecutive differences.
```
theorem prefixCoordinateEquiv_symm_increment (n : ℕ) (y : Fin (n + 1) → G) (i : Fin n) :
    (prefixCoordinateEquiv (n + 1)).symm y i.succ = (y i.castSucc)⁻¹ * y i.succ := by
…
```
Mentions: OAI.PolycyclicRecognition.prefixCoordinateEquiv
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_symm_zero line 69
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_symm_mul_increment line 76
Source documentation
Thickening the total lifts on the right changes an increment only by the correction on its left and the correction on its right.
```
theorem prefixCoordinateEquiv_symm_mul_increment (n : ℕ)
    (y η : Fin (n + 1) → G) (i : Fin n) :
    (prefixCoordinateEquiv (n + 1)).symm (fun j => y j * η j) i.succ =
      (η i.castSucc)⁻¹ * (prefixCoordinateEquiv (n + 1)).symm y i.succ * η i.succ := by
…
```
Mentions: OAI.PolycyclicRecognition.prefixCoordinateEquiv
theorem OAI.PolycyclicRecognition.continuous_prefixCoordinateEquiv_symm line 83
theorem OAI.PolycyclicRecognition.measurePreserving_prefixCoordinateEquiv line 101
theorem OAI.PolycyclicRecognition.measurePreserving_prefixCoordinateEquiv_symm line 124
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_symm_image_measure line 130