OAI/Geometry/PinnedDistances/ArithmeticGraphs.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.PreparedGraph.edgeCount_pos line 36
2. lemma OAI.WeakPinned.PreparedGraph.edge_domination line 42
3. lemma OAI.WeakPinned.PreparedGraph.degree_law line 58
4. lemma OAI.WeakPinned.PreparedGraph.heavy_bound line 77
5. lemma OAI.WeakPinned.PreparedGraph.small_heavy_bound line 97
6. def OAI.WeakPinned.Core.Fibers.qCell line 124
7. lemma OAI.WeakPinned.Core.Fibers.qCell_eq line 126
8. lemma OAI.WeakPinned.Core.Fibers.fiber_mass line 132
9. lemma OAI.WeakPinned.Core.Fibers.qCell_split line 136
10. lemma OAI.WeakPinned.Core.Fibers.qCell_bound line 159
11. lemma OAI.WeakPinned.Variance.weighted_pair line 171
12. lemma OAI.WeakPinned.Variance.weighted_additive line 190
13. lemma OAI.WeakPinned.Variance.uniform_additive line 209
14. lemma OAI.WeakPinned.PreparedGraph.overlap_lower line 233
15. lemma OAI.WeakPinned.PreparedGraph.small_overlap line 251

    Source documentation

    A fully quantitative version of small-overlap before either scale branch. The slice is the actual original fiber mass, not an assumed error term.

    lemma PreparedGraph.small_overlap (h : PreparedGraph V I G θ γ c η) (hη : η<θ) (hη0 : 0≤η)
        (m : Finset V → ℝ) (hm : ∀ C, 0 ≤ m C) (b : ℝ) (S : V → ℝ) (hS : ∀ x, 0≤S x)
        (hL : ∀ x y, x≠y → weightedOverlap m x y=b+S x+S y) :
        (θ/(θ-η))*weightedIntegral m (fun C => if (C.card : ℝ)≤(Fintype.card V : ℝ)^(1-c)
          then pairCell Finset.univ C else 0) ≤
          weightedIntegral m (slice G.fiberWeight (fun e => prob (G.targets e)) G.source (1/Real.log (Fintype.card V : ℝ))) +
          ((θ+η)/(θ-η)-1)*weightedIntegral m (pairCell Finset.univ) +
          (2-2*((θ-η)/(θ+η/8)))*(∑ x, prob Finset.univ x*S x) := by
    …

    Mentions: OAI.WeakPinned.PreparedGraph

16. def OAI.WeakPinned.overlapScale line 298
17. def OAI.WeakPinned.potentialScale line 299
18. def OAI.WeakPinned.smallOverlapScale line 301
19. lemma OAI.WeakPinned.overlapScale_nonneg line 304
20. lemma OAI.WeakPinned.potentialScale_nonneg line 307
21. lemma OAI.WeakPinned.smallOverlapScale_nonneg line 314
22. lemma OAI.WeakPinned.PreparedGraph.arithmetic_slice line 323
23. lemma OAI.WeakPinned.PreparedGraph.arithmetic_small_overlap line 359

    Source documentation

    The genuine scale estimate, valid for every prepared arithmetic model. All error terms are explicit and can be sent to zero uniformly in the field.

    lemma PreparedGraph.arithmetic_small_overlap (h : PreparedGraph V I G θ γ c η) (hη : η < θ) (hη0 : 0 ≤ η)
        (t : I → K) (ht : ∀ e y, y ∈ G.targets e → (Z₁ (G.source e)-Z₁ y)*(Z₂ (G.source e)-Z₂ y)=t e)
        (τ H : ℝ) (hlam : 0 ≤ 1/Real.log (Fintype.card V:ℝ)) (hlam2 : 1/Real.log (Fintype.card V:ℝ) ≤ 1/2)
        (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hτn : 2 ≤ τ*(Fintype.card V:ℝ)) (hH : 0 ≤ H) :
        smallOverlapScale Z₁ Z₂ h₁ h₂ c ≤
          (2*(1/Real.log (Fintype.card V:ℝ))/τ^2+2*(1/Real.log (Fintype.card V:ℝ))/(θ-η)+((θ+η)/(θ-η)-1))*overlapScale Z₁ Z₂ h₁ h₂ +
          (2*τ/(θ-η)+(2-2*((θ-η)/(θ+η/8))))*potentialScale Z₁ Z₂ h₁ h₂ +
          4*(1/Real.log (Fintype.card V:ℝ))*H + 32*Real.exp (-H/2) := by
    …

    Mentions: OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.smallOverlapScale, OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale

24. lemma OAI.WeakPinned.Variance.varianceCell_nonneg line 382
25. lemma OAI.WeakPinned.Variance.reciprocal_card_sub_one line 393
26. theorem OAI.WeakPinned.arithmetic_variance_rate line 410

    Source documentation

    Asymptotic arithmetic variance for arbitrary genuine uniform-subset families. The domination and size assumptions are finite sampling data. The exact arithmetic cancellation and small-overlap rate are already proved.

    theorem arithmetic_variance_rate (w : ∀ j, I j → ℝ) (B : ∀ j, I j → Finset (V j))
        (γ c M₀ : ℝ) (hγ : 0<γ) (hγ1 : γ<1) (hcγ : c<γ) (_hc1 : c<1) (hM : 0≤M₀)
        (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
        (hw : ∀ j i, 0≤w j i) (hW : ∀ j, (∑ i, w j i)≤1)
        (hsize : ∀ᶠ j in atTop, ∀ i, (Fintype.card (V j):ℝ)^γ ≤ ((B j i).card:ℝ))
        (hdom : ∀ᶠ j in atTop, ∀ x, (∑ i, w j i*prob (B j i) x)≤ M₀*prob Finset.univ x)
        (hsmall : Tendsto (fun j => smallOverlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j) c /
          (overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+potentialScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+1)) atTop (𝓝 0)) :
        Tendsto (fun j => weightedIntegral (totalMass (Z₁ j) (Z₂ j) (h₁ j) (h₂ j))
          (varianceCell (w j) (B j) ((Fintype.card (V j):ℝ)^(1-c))) /
          (overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+potentialScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+1)) atTop (𝓝 0) := by
    …

    Mentions: OAI.WeakPinned.B, OAI.WeakPinned.smallOverlapScale, OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale