OAI/GroupTheory/PolycyclicRecognition/Analysis/WordBallSamplingSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting actual bounded chart maps at eventual sampling scales

  1. theorem OAI.PolycyclicRecognition.exists_wordBall_sampling_sequence line 16

    Source documentation

    The geometric witnesses can be selected along a sequence together with continuous compact-ball chart maps. Early indices impose no conditions.

    theorem exists_wordBall_sampling_sequence
    {L E G N : Type*} [LieRing L] [LieAlgebra โ„ L]
    [NormedAddCommGroup E] [NormedSpace โ„ E] [FiniteDimensional โ„ E]
    [TopologicalSpace G] [ChartedSpace E G] [Group G]
    [LieGroup (๐“˜(โ„, E)) โŠค G] [IsTopologicalGroup G]
    [MeasurableSpace N] [Nonempty N]
    (e : L โ‰ƒโ‚—โ…โ„โ† GroupLieAlgebra (๐“˜(โ„, E)) G)
    (chart : GroupLieAlgebra (๐“˜(โ„, E)) G โ‰ƒโ‚œ G)
    {d : โ„•} (source target : โ„• โ†’ Basis (Fin d) โ„ L)
    {R S : โ„} (hS : 0 โ‰ค S)
    (P : โ„• โ†’ N โ†’ G โ†’ ProbabilityMeasure N โ†’ Prop)
    (hP : โˆ€แถ  n in atTop, โˆƒ (u : N) (k : G) (ฮฝ : ProbabilityMeasure N),
โ€ฆ