OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.NeighborSamplingRow.distance_tendsto_zero line 45

   Source documentation

   Portmanteau is applied to the original Haar samples, retaining the actual neighboring law rather than replacing it by an abstract measure.

   theorem NeighborSamplingRow.distance_tendsto_zero
       (Z : Set (Fin (finrank ℝ H) → ℝ)) [CompactSpace Z]
       (hpoints : ∀ f ∈ (D.law : Measure (Profiles × Profiles)).support,
         ∀ z ∈ Z, f.1.val z = f.2.val z)
       {η : ℝ} (hη : 0 < η) :
       Tendsto (fun n => (M.translatedGroupBoxProbability T F hunimod eW
         haarN chartN hchartN bN cell β (D.scale n) (D.base n) : Measure F.N.carrier)
         {q | η ≤ dist ((D.profile n q).val.restrict Z)
           ((D.profile n (q * D.step n)).val.restrict Z)}) atTop (𝓝 0) := by
   …