NormalizedGraphs.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.WeakPinned.Bounded.normalized_graph_impossible line 18

Source documentation

Compactness is applied to the four genuine empirical graph laws together. The only asymptotic hypotheses are the proved test-discrepancy estimates.

theorem normalized_graph_impossible
    (G : ∀ n,Core.Fibers (V n) (I n)) (u₁ u₂ : ∀ n,V n → ℂ)
    (x₁ x₂ : ∀ n,V n) (hu₁ : ∀ n,Function.Injective (u₁ n)) (hu₂ : ∀ n,Function.Injective (u₂ n))
    (hG : ∀ n,0<(G n).edgeCount) (hB : ∀ n e,((G n).targets e).Nonempty)
    (hn : ∀ n,2≤Fintype.card (V n))
    (hcard : Tendsto (fun n => (Fintype.card (V n):ℝ)) atTop atTop)
    (C : ℝ) (hC : 0≤C) (hlog₁ : ∀ n,logAverage (u₁ n)≤C) (hlog₂ : ∀ n,logAverage (u₂ n)≤C)
    (hx₁ : ∀ n,(∑ y,logCost (u₁ n) (x₁ n) y)≤C*(Fintype.card (V n):ℝ))
    (hx₂ : ∀ n,(∑ y,logCost (u₂ n) (x₂ n) y)≤C*(Fintype.card (V n):ℝ))
    (hd₁ : ∀ f : C(Sphere,ℝ),Tendsto (fun n => testDiscrep (G n).fiberWeight (G n).targets
      (fun x => f ((u₁ n x-u₁ n (x₁ n)):Sphere))) atTop (𝓝 0))
    (hd₂ : ∀ f : C(Sphere,ℝ),Tendsto (fun n => testDiscrep (G n).fiberWeight (G n).targets
…

Mentions: OAI.WeakPinned.Core.Fibers, OAI.WeakPinned.Bounded.logAverage, OAI.WeakPinned.Bounded.logCost, OAI.WeakPinned.Bounded.Sphere, OAI.WeakPinned.Bounded.testDiscrep