OAI/GroupTheory/PolycyclicRecognition/Analysis/SectionSubtypeProbePacking.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_dilated_section_subtype_probe_counts line 28

   Source documentation

   Compact good probes selected on the original product cell give the actual separated image count. Their subtype probability is transported exactly; the choice of starting sample causes no loss of source volume.

   theorem exists_dilated_section_subtype_probe_counts
       (π : N →* Q) (hπ : Continuous π) (σ : C(Q, N)) (hs : ∀ q, π (σ q) = q)
       (μQ : Measure Q) (μI : Measure π.ker) [SFinite μQ] [SFinite μI]
       (μ : Measure N) [μ.IsMulLeftInvariant] [IsFiniteMeasureOnCompacts μ]
       (hμ : μ = Measure.map (quotientSectionHomeomorph π hπ σ hs).symm (μQ.prod μI))
       (ι : N →* G) (κ : D →* G) (φ : D →* MulAut N)
       (hι : Topology.IsClosedEmbedding ι)
       (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
       (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (S : ℕ → N ≃ₜ N) (hS : ∀ n, MeasurePreserving (S n) μ μ)
       {Λ : ℝ≥0} (hΛ : 0 < (Λ : ℝ)) (p : ℕ → NormalizedPair G Λ)
       (x a : ℕ → G) (d : ℕ → D)
   …

   Mentions: OAI.PolycyclicRecognition.quotientSectionHomeomorph, OAI.PolycyclicRecognition.NormalizedPair

2. theorem OAI.PolycyclicRecognition.exists_absolute_section_subtype_probe_counts line 82

   Source documentation

   For normalized quasi-isometries the source net consists of the actual image points. The count and separation are unchanged, and the image witnesses now match the two-path offset theorem directly.

   theorem exists_absolute_section_subtype_probe_counts
       (π : N →* Q) (hπ : Continuous π) (σ : C(Q, N)) (hs : ∀ q, π (σ q) = q)
       (μQ : Measure Q) (μI : Measure π.ker) [SFinite μQ] [SFinite μI]
       (μ : Measure N) [μ.IsMulLeftInvariant] [IsFiniteMeasureOnCompacts μ]
       (hμ : μ = Measure.map (quotientSectionHomeomorph π hπ σ hs).symm (μQ.prod μI))
       (ι : N →* G) (κ : D →* G) (φ : D →* MulAut N)
       (hι : Topology.IsClosedEmbedding ι)
       (hφ : ∀ d, MeasurePreserving (φ d) μ μ)
       (hconj : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (S : ℕ → N ≃ₜ N) (hS : ∀ n, MeasurePreserving (S n) μ μ)
       {Λ : ℝ≥0} (hΛ : 0 < (Λ : ℝ)) (p : ℕ → NormalizedPair G Λ)
       (x : ℕ → G) (d : ℕ → D)
   …

   Mentions: OAI.PolycyclicRecognition.quotientSectionHomeomorph, OAI.PolycyclicRecognition.NormalizedPair