SectionProbeReparametrization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Probe coordinates on the original quotient/kernel cell

The sampling law may be chosen on the original Haar cell and composed with this homeomorphism. Thus the compact set selected by concentration is already measured by the probability law required by source packing.

def OAI.PolycyclicRecognition.sectionProbeCoordinates line 23
Source documentation
Coordinates of a point of the actual quotient/kernel product cell.
```
def sectionProbeCoordinates (eQ : Z ≃ₜ Q) (eI : I ≃ₜ K) (B : Set Z) (U : Set I) :
    ((eQ '' B) ×ˢ (eI '' U)) ≃ₜ B × U :=
…
```
theorem OAI.PolycyclicRecognition.sectionProbeCoordinates_fst line 28
theorem OAI.PolycyclicRecognition.sectionProbeCoordinates_snd line 34
def OAI.PolycyclicRecognition.coordinateQuotientSection line 44
Source documentation
The section selected in linear quotient coordinates is an actual continuous section on the quotient group.
```
def coordinateQuotientSection (eQ : Z ≃ₜ Q) (σ : C(Z, N)) : C(Q, N) :=
…
```
theorem OAI.PolycyclicRecognition.coordinateQuotientSection_rightInverse line 47

theorem OAI.PolycyclicRecognition.reparametrized_probe_first line 55

Source documentation

The counted probe endpoint is exactly kernel coordinate times section coordinate in the original Haar product cell.

theorem reparametrized_probe_first
    [Mul N] (eQ : Z ≃ₜ Q) (eI : I ≃ₜ K) (B : Set Z) (U : Set I)
    (ι : I → N) (inc : K → N) (hι : ∀ i, inc (eI i) = ι i)
    (σ : C(Z, N)) (probe : B × U → N)
    (hprobe : ∀ y, probe y = ι y.2.val * σ y.1.val)
    (y : (eQ '' B) ×ˢ (eI '' U)) :
    probe (sectionProbeCoordinates eQ eI B U y) =
      inc y.val.2 * coordinateQuotientSection eQ σ y.val.1 := by
…

Mentions: OAI.PolycyclicRecognition.sectionProbeCoordinates, OAI.PolycyclicRecognition.coordinateQuotientSection