OAI/Geometry/PinnedDistances/GlobalOverlap.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Grid.truncated_error_integrable line 27
2. lemma OAI.WeakPinned.Grid.truncated_error_mean line 31
3. lemma OAI.WeakPinned.Grid.truncated_sum_bound line 72
4. lemma OAI.WeakPinned.Grid.paired_error_mean line 83
5. lemma OAI.WeakPinned.Global.arch_fiber_defect line 111
6. lemma OAI.WeakPinned.Global.arch_defect_mean line 125
7. lemma OAI.WeakPinned.Global.arch_weighted_defect line 138
8. lemma OAI.WeakPinned.Global.arch_small_fiber line 165
9. lemma OAI.WeakPinned.Global.finite_small_fiber line 222
10. lemma OAI.WeakPinned.Global.finite_zero_outside line 250
11. lemma OAI.WeakPinned.Global.finite_mass_zero line 261
12. lemma OAI.WeakPinned.Global.sum_finite_mass line 272
13. lemma OAI.WeakPinned.Global.sum_finite_potential line 279
14. def OAI.WeakPinned.Global.placeAverage line 287
15. lemma OAI.WeakPinned.Global.placeAverage_mono line 291
16. lemma OAI.WeakPinned.Global.placeAverage_add line 298
17. lemma OAI.WeakPinned.Global.placeAverage_mul line 304
18. lemma OAI.WeakPinned.Global.placeAverage_arch_const line 312
19. lemma OAI.WeakPinned.Global.cellIntegral_placeAverage line 317
20. lemma OAI.WeakPinned.Global.potentialIntegral_placeAverage line 334
21. lemma OAI.WeakPinned.Global.arithmetic_small_fiber_one line 346
22. lemma OAI.WeakPinned.Global.arithmetic_small_fiber line 379

    Source documentation

    The global small-fiber estimate, uniformly over number fields, places and configurations.

    lemma arithmetic_small_fiber (hn : 2 ≤ Fintype.card P)
        (w : I → ℝ) (p : I → P → ℝ) (x : I → P) (t : I → K)
        (hw : ∀ i, 0 ≤ w i) (hW : ∑ i, w i=1) (hp : ∀ i y, 0 ≤ p i y)
        (hp1 : ∀ i, ∑ y, p i y=1) (hx : ∀ i, p i (x i)=0)
        (ht : ∀ i y, p i y ≠ 0 → (Z₁ (x i)-Z₁ y)*(Z₂ (x i)-Z₂ y)=t i)
        (B τ lam H : ℝ) (hB : 0 ≤ B) (hlam : 0 ≤ lam) (hlam2 : lam ≤ 1/2)
        (hτ : 0 < τ) (hτ1 : τ ≤ 1) (hτn : 2 ≤ τ*(Fintype.card P:ℝ)) (hH : 0 ≤ H)
        (hdom : ∀ a b, a ≠ b → edgeLaw w p x a b ≤ B/((Fintype.card P:ℝ)*((Fintype.card P:ℝ)-1))) :
        weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (slice w p x lam) ≤
          (2*lam/τ^2+2*lam*B)*weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (pairCell Finset.univ) +
          2*B*τ/(Fintype.card P:ℝ)*(∑ y, totalPotential Z₁ Z₂ h₁ h₂ y) + 4*lam*H +
          32*Real.exp (-H/2) := by
    …

    Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Global.totalMass, OAI.WeakPinned.Global.totalPotential