OAI/Geometry/PinnedDistances/OverlapRates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakPinned.small_overlap_rate line 36

   Source documentation

   The scalar limiting step for small overlap, with fixed positive τ and H.

   theorem small_overlap_rate (n η U A D : ℕ → ℝ) (θ : ℝ) (hθ : 0 < θ)
       (hn : Tendsto n atTop atTop) (hη : Tendsto η atTop (𝓝 0))
       (hη0 : ∀ j, 0 ≤ η j) (hU : ∀ j, 0 ≤ U j) (hA : ∀ j, 0 ≤ A j) (hD : ∀ j, 0 ≤ D j)
       (hbound : ∀ τ H : ℝ, 0 < τ → τ ≤ 1 → 0 ≤ H → ∀ᶠ j in atTop,
         D j ≤ (2*(1/Real.log (n j))/τ^2+2*(1/Real.log (n j))/(θ-η j)+((θ+η j)/(θ-η j)-1))*U j +
           (2*τ/(θ-η j)+(2-2*((θ-η j)/(θ+η j/8))))*A j +
           4*(1/Real.log (n j))*H + 32*Real.exp (-H/2)) :
       Tendsto (fun j => D j/(U j+A j+1)) atTop (𝓝 0) := by
   …

2. theorem OAI.WeakPinned.arithmetic_small_overlap_rate line 124

   Source documentation

   Application of the scalar rate to the genuinely prepared arithmetic graphs, with no degree bound on the sequence of number fields.

   theorem arithmetic_small_overlap_rate (hθ : 0<θ)
       (hn : Tendsto (fun j => (Fintype.card (V j) : ℝ)) atTop atTop)
       (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j, 0≤η j)
       (hG : ∀ j, PreparedGraph (V j) (I j) (G j) θ γ c (η j))
       (t : ∀ j, I j → K j)
       (ht : ∀ j e y, y ∈ (G j).targets e →
         (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e) :
       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) := by
   …

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

3. def OAI.WeakPinned.Core.Fibers.retainedWeight line 158
4. def OAI.WeakPinned.Core.Fibers.retainedSet line 160
5. lemma OAI.WeakPinned.Core.Fibers.retainedWeight_nonneg line 163
6. lemma OAI.WeakPinned.Core.Fibers.retainedWeight_le line 168
7. lemma OAI.WeakPinned.Core.Fibers.sum_retainedWeight line 175
8. lemma OAI.WeakPinned.Core.Fibers.retainedSet_size line 180
9. lemma OAI.WeakPinned.Core.Fibers.retained_domination line 187
10. lemma OAI.WeakPinned.PreparedGraph.uniform_domination line 207
11. def OAI.WeakPinned.fiberVariance line 221
12. def OAI.WeakPinned.incomingVariance line 224
13. theorem OAI.WeakPinned.sampling_variance_rates line 231

    Source documentation

    Both source sampling families satisfy the proved vanishing arithmetic variance estimate, on every sequence of prepared models. No uniform degree bound on the number fields is used.

    theorem sampling_variance_rates (hθ : 0<θ) (hγ : 0<γ) (hγ1 : γ<1) (hcγ : c<γ)
        (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
        (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j, 0≤η j) (hηb : ∀ j, η j≤θ/2)
        (hG : ∀ j, PreparedGraph (V j) (I j) (G j) θ γ c (η j))
        (t : ∀ j, I j → K j) (ht : ∀ j e y, y ∈ (G j).targets e →
          (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e) :
        Tendsto (fun j => fiberVariance G c Z₁ Z₂ h₁ h₂ j /
          (overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+potentialScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+1)) atTop (𝓝 0) ∧
        Tendsto (fun j => incomingVariance G γ c Z₁ Z₂ h₁ h₂ j /
          (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.PreparedGraph, OAI.WeakPinned.fiberVariance, OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale, OAI.WeakPinned.incomingVariance