OAI/Geometry/PinnedDistances/GlobalPotentials.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Global.placeUnion line 44
2. def OAI.WeakPinned.Global.average line 48
3. def OAI.WeakPinned.Global.AverageIntegrable line 54
4. lemma OAI.WeakPinned.Global.average_mono line 58
5. lemma OAI.WeakPinned.Global.average_add line 71
6. lemma OAI.WeakPinned.Global.average_mul line 80
7. lemma OAI.WeakPinned.Global.average_sum line 87
8. lemma OAI.WeakPinned.Global.average_potential_left line 97
9. lemma OAI.WeakPinned.Global.average_potential_right line 104
10. lemma OAI.WeakPinned.Global.average_mass_left line 111
11. lemma OAI.WeakPinned.Global.average_mass_right line 118
12. lemma OAI.WeakPinned.Global.integrable_potential_left line 127
13. lemma OAI.WeakPinned.Global.integrable_potential_right line 134
14. lemma OAI.WeakPinned.Global.integrable_mass_left line 141
15. lemma OAI.WeakPinned.Global.integrable_mass_right line 148
16. def OAI.WeakPinned.Global.potentialEval line 163
17. def OAI.WeakPinned.Global.massEval line 165
18. lemma OAI.WeakPinned.Global.integrable_potentialEval line 170
19. lemma OAI.WeakPinned.Global.integrable_massEval line 179
20. lemma OAI.WeakPinned.Global.average_potentialEval line 187
21. lemma OAI.WeakPinned.Global.average_massEval line 200
22. lemma OAI.WeakPinned.Global.massEval_edge line 217
23. lemma OAI.WeakPinned.Global.potentialEval_mixture line 248
24. lemma OAI.WeakPinned.Global.average_sub line 253
25. lemma OAI.WeakPinned.Global.arithmetic_potential_fiber_bound line 264

    Source documentation

    The first-moment raw-depth error is archimedean only. Its global constant is independent of the degree and all coordinates.

    lemma arithmetic_potential_fiber_bound (hn : 2≤Fintype.card P)
        (w : I → ℝ) (B : I → Finset P) (src : I → P) (t : I → K) (T M κ : ℝ)
        (hw : ∀ i, 0≤w i) (hW : (∑ i, w i)=1) (hT : 1≤T) (hκ : 0≤κ)
        (hB : ∀ i, 2≤(B i).card) (hk : ∀ i, 2/((B i).card:ℝ)≤κ)
        (hsrc : ∀ i, src i∉B i)
        (hdom : ∀ x, (∑ i, w i*prob (B i) x)≤M*prob Finset.univ x)
        (ht : ∀ i y, y∈B i → (Z₁ (src i)-Z₁ y)*(Z₂ (src i)-Z₂ y)=t i) :
        (∑ y, (∑ i, w i*prob (B i) y)*totalPotential Z₁ Z₂ h₁ h₂ y) ≤
          4*weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (varianceCell w B T)+
          8*overlapScale Z₁ Z₂ h₁ h₂+
          2*κ*M*potentialScale Z₁ Z₂ h₁ h₂+
          weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (SmallFiber.edgeCell w (fun i => prob (B i)) src)+16 := by
    …

    Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Global.M, OAI.WeakPinned.Global.totalPotential, OAI.WeakPinned.Global.totalMass, OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale, OAI.WeakPinned.SmallFiber.edgeCell

26. lemma OAI.WeakPinned.Variance.point_potential_lower line 358

    Source documentation

    Nonnegative additive off-diagonal overlap controls the potential at every vertex, not merely at vertices typical for the edge marginal.

    lemma point_potential_lower (m : Finset P → ℝ) (b : ℝ) (S : P → ℝ)
        (hm : ∀ C : Finset P, (0 : ℝ) ≤ m C) (hL : ∀ x y, x≠y → weightedOverlap m x y=b+S x+S y)
        (hn : 3≤Fintype.card P) (x : P) :
        (∑ y, prob Finset.univ y*S y)-2*weightedIntegral m (pairCell Finset.univ)≤S x := by
    …

    Mentions: OAI.WeakPinned.Variance.weightedOverlap, OAI.WeakPinned.Variance.prob, OAI.WeakPinned.Variance.weightedIntegral, OAI.WeakPinned.Variance.pairCell

27. theorem OAI.WeakPinned.arithmetic_scale_balance line 398

    Source documentation

    Quantitative scale balance for arithmetic fibers, without an unboundedness assumption.

    theorem arithmetic_scale_balance (G : Core.Fibers P I)
        (Z₁ Z₂ : P → K) (h₁ : Function.Injective Z₁) (h₂ : Function.Injective Z₂)
        (hn : 3≤Fintype.card P) (hG : 0<G.edgeCount)
        (T M κ : ℝ) (hT : 1≤T) (hκ : 0≤κ)
        (hB : ∀ i, 2≤(G.targets i).card) (hk : ∀ i, 2/((G.targets i).card:ℝ)≤κ)
        (hdom : ∀ x y, G.edgeLaw x y≤M*pairProb Finset.univ x y)
        (t : I → K) (ht : ∀ i y, y∈G.targets i →
          (Z₁ (G.source i)-Z₁ y)*(Z₂ (G.source i)-Z₂ y)=t i) :
        (1-2*κ*M)*potentialScale Z₁ Z₂ h₁ h₂ ≤
          4*weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (varianceCell G.fiberWeight G.targets T)+
          (10+M)*overlapScale Z₁ Z₂ h₁ h₂+16 := by
    …

    Mentions: OAI.WeakPinned.Core.Fibers, OAI.WeakPinned.potentialScale, OAI.WeakPinned.overlapScale

28. lemma OAI.WeakPinned.scale_balance_rate line 452

    Source documentation

    Elementary absorption of the two asymptotically small errors.

    lemma scale_balance_rate (W A V δ : ℕ → ℝ) (B : ℝ) (hB : 0≤B)
        (hW : ∀ j, 0≤W j) (hA : ∀ j, 0≤A j)
        (hδ : Tendsto δ atTop (𝓝 0))
        (hV : Tendsto (fun j => V j/(W j+A j+1)) atTop (𝓝 0))
        (hbal : ∀ᶠ j in atTop, (1-δ j)*A j≤4*V j+(10+B)*W j+16) :
        ∀ᶠ j in atTop, A j≤(64+4*B)*(W j+1) := by
    …

    Mentions: OAI.WeakPinned.B

29. theorem OAI.WeakPinned.arithmetic_scale_comparison line 473