CartanSourceOffsetComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The offset comparison for the actual tiled and linked probes

theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.offset_nonpos_of_source_geometry line 78

Source documentation

Specialization to the actual tiled source cell with group-valued geometry.

theorem TiledProbeChainData.offset_nonpos_of_source_geometry
    (πT : F.N.carrier →* QT) (hπT : Continuous πT)
    (μT : Measure QT) (μTI : Measure πT.ker)
    (μ : Measure F.N.carrier) (ν : Measure F.D.carrier)
    [SFinite μT] [SFinite μTI] [SFinite μ] [SFinite ν]
    [μT.IsMulLeftInvariant] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant]
    (hφ : ∀ d, MeasurePreserving (F.action d) μ μ)
    (actionQ : F.D.carrier →* MulAut QT) (act : G →* Equiv.Perm QT)
    (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = πT u * actionQ d q)
    (hscale : Tendsto scale atTop atTop) (hscale0 : ∀ n, 0 < scale n)
    (P₂ : ℝ) (regions : MeasuredProbeRegions πT μT μTI ν scale P₂)
    (hμ : μ = Measure.map (quotientSectionHomeomorph πT hπT
…

Mentions: OAI.PolycyclicRecognition.MeasuredProbeRegions, OAI.PolycyclicRecognition.quotientSectionHomeomorph