OAI/GroupTheory/PolycyclicRecognition/Analysis/PairChainSublinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.pairHeight_sublinear_of_linearChains line 23

   Source documentation

   The compact-uniform transfer estimate gives sublinearity for the compatible metric selected by the published metric-existence input.

   theorem pairHeight_sublinear_of_linearChains
       (μ : Measure (NormalizedPair G Λ)) [IsFiniteMeasure μ]
       [SMulInvariantMeasure G (NormalizedPair G Λ) μ]
       (C : LinearMetricChains G)
       (π l : G →* Multiplicative W) (hπ : Continuous fun g => (π g).toAdd)
       (φ : ℕ → NormalizedPair G Λ → W) (hφ : ∀ n, MemLp (φ n) 2 μ)
       (happrox : ∀ Q : Set G, IsCompact Q →
         Filter.Tendsto (fun n => ⨆ t ∈ Q,
           ∫⁻ p, ‖pairTransferDefect π l (φ n) t p‖ₑ ^ 2 ∂μ) Filter.atTop (nhds 0)) :
       ∀ ε : ℝ, 0 < ε → ∃ B : ℝ, 0 ≤ B ∧ ∀ g,
         ‖pairHeightL2 μ π hπ g - Lp.const 2 μ (l g).toAdd‖ ≤ ε * dist 1 g + B := by
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairTransferDefect, OAI.PolycyclicRecognition.pairHeightL2

2. theorem OAI.PolycyclicRecognition.inverseCoupling_sublinear_of_linearChains line 48

   Source documentation

   The actual inverse coupling supplies a sublinear inverse height error with exactly the inverse coefficient. No ergodicity of its finite measure and no second reduced-cohomology hypothesis are required. The metric assumption is precisely the published large-scale chain condition.

   theorem inverseCoupling_sublinear_of_linearChains
       {G W : Type*} [Group G] [MetricSpace G] [ProperSpace G]
       [SecondCountableTopology G] [IsTopologicalGroup G] [IsIsometricSMul G G]
       {Λ : ℝ≥0} [MeasurableSpace G] [BorelSpace G]
       [MeasurableSpace (NormalizedPair G Λ)] [BorelSpace (NormalizedPair G Λ)]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] [SecondCountableTopology W]
       [MeasurableSpace W] [BorelSpace W]
       (m : Measure G) [m.IsHaarMeasure] [m.IsMulRightInvariant]
       (μ : Measure (NormalizedPair G Λ)) [IsProbabilityMeasure μ]
       [SMulInvariantMeasure G (NormalizedPair G Λ) μ]
       (A : W ≃L[ℝ] W) (π l : G →* Multiplicative W)
       (hπ : Continuous fun g => (π g).toAdd) (hl : Continuous fun g => (l g).toAdd)
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair