OAI/Geometry/PinnedDistances/LimitObstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakPinned.Bounded.graph_limit_impossible line 18

   Source documentation

   The actual finite expanded graph laws cannot have nonatomic coordinate limits and the two test-independence properties supplied by the variance estimates.

   theorem graph_limit_impossible
       (G : ∀ n,Core.Fibers (V n) (I n)) (U₁ U₂ : ∀ n,V n → ℂ)
       (hG : ∀ n,0<(G n).edgeCount) (hB : ∀ n e,((G n).targets e).Nonempty)
       (hn : ∀ n,2≤Fintype.card (V n))
       (β₁ β₂ : ProbabilityMeasure Sphere) (Q : ProbabilityMeasure (Quad Sphere))
       (R : ProbabilityMeasure (Expanded Sphere))
       [NullSingletonClass (β₁:Measure Sphere)] [NullSingletonClass (β₂:Measure Sphere)]
       (hα₁ : Tendsto (fun n => uniformProbability (fun x => (U₁ n x:Sphere)) (by have:=hn n;omega)) atTop (𝓝 β₁))
   …

   Mentions: OAI.WeakPinned.Core.Fibers, OAI.WeakPinned.Bounded.Sphere, OAI.WeakPinned.Bounded.Quad, OAI.WeakPinned.Bounded.Expanded, OAI.WeakPinned.Bounded.uniformProbability