OAI/Geometry/PinnedDistances/MinPotentials.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Variance.cell_second_moment line 38

   Source documentation

   The giant-complement second moment estimate needed to compare W and W₂. The linear error, unlike an absolute singleton error, can be integrated.

   lemma cell_second_moment (w : I → ℝ) (B : I → Finset P) (T M κ : ℝ)
       (hw : ∀ i, 0≤w i) (hW : (∑ i, w i)≤1) (hT : 1≤T) (hκ : 0≤κ)
       (hk : ∀ i, 2/((B i).card:ℝ)≤κ)
       (hdom : ∀ x, (∑ i, w i*prob (B i) x)≤M*prob Finset.univ x) (C : Finset P) :
       (∑ i, w i*(cellProb (B i) C)^2) ≤
         2*varianceCell w B T C + 4*pairCell Finset.univ C + κ*M*cellProb Finset.univ C := by
   …

   Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Variance.prob, OAI.WeakPinned.Variance.cellProb, OAI.WeakPinned.Variance.varianceCell, OAI.WeakPinned.Variance.pairCell

2. lemma OAI.WeakPinned.Variance.small_mass_qCell line 79

   Source documentation

   Small positive-mass cut contributions are slice contributions or variance.

   lemma small_mass_qCell {w : I → ℝ} {B : I → Finset P} (src : I → P) (T δ : ℝ)
       (hw : ∀ i, 0≤w i) (hδ : 0<δ) (hk : ∀ i, 2/((B i).card:ℝ)≤2*δ)
       (C : Finset P) (hC : cellProb Finset.univ C≤δ) :
       (∑ i, w i*(if src i ∈ C then cellProb (B i) C else 0)) ≤
         (∑ i, w i*(if src i ∈ C ∧ cellProb (B i) C<2*δ then cellProb (B i) C else 0)) +
         (2/δ)*varianceCell w B T C := by
   …

   Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Variance.cellProb, OAI.WeakPinned.Variance.varianceCell

3. lemma OAI.WeakPinned.Hierarchy.Depth.mem_giant_iff_cell line 129
4. lemma OAI.WeakPinned.Hierarchy.Depth.mem_giant_exists line 141
5. lemma OAI.WeakPinned.Hierarchy.Depth.mem_giant_mono line 152
6. lemma OAI.WeakPinned.Hierarchy.Depth.isClosed_mem_giant line 157
7. lemma OAI.WeakPinned.Hierarchy.Depth.mem_giant_low line 174
8. lemma OAI.WeakPinned.Hierarchy.Depth.mem_giant_le_M line 178
9. def OAI.WeakPinned.Hierarchy.Depth.departure line 183

   Source documentation

   The last level at which the vertex belongs to the nested giant.

   def departure (x : P) : ℝ := sSup {r : ℝ | x ∈ d.giant r}

10. lemma OAI.WeakPinned.Hierarchy.Depth.departure_cutoff line 185
11. lemma OAI.WeakPinned.Hierarchy.Depth.departure_le_M line 191
12. lemma OAI.WeakPinned.Hierarchy.Depth.outside_departure line 194
13. lemma OAI.WeakPinned.Hierarchy.Depth.integral_one_Ioc line 201
14. lemma OAI.WeakPinned.Hierarchy.Depth.potential_departure line 206
15. lemma OAI.WeakPinned.Hierarchy.Depth.outside_product line 210
16. lemma OAI.WeakPinned.Hierarchy.Depth.min_potential line 219

    Source documentation

    Exact layer-cake identity, including the finite set of threshold ties.

    lemma min_potential (hn : 2 ≤ Fintype.card P) (x y : P) :
        min (d.potential x) (d.potential y) = ∫ r, d.outsideIndicator r x*d.outsideIndicator r y := by
    …

17. def OAI.WeakPinned.MinKernel.step line 233
18. lemma OAI.WeakPinned.MinKernel.integrable_step line 235
19. lemma OAI.WeakPinned.MinKernel.step_mul line 239
20. lemma OAI.WeakPinned.MinKernel.integral_step line 244
21. def OAI.WeakPinned.MinKernel.tail line 248
22. def OAI.WeakPinned.MinKernel.energy line 250
23. lemma OAI.WeakPinned.MinKernel.tail_product line 252
24. lemma OAI.WeakPinned.MinKernel.integrable_tail_product line 265
25. lemma OAI.WeakPinned.MinKernel.energy_integral line 270
26. lemma OAI.WeakPinned.MinKernel.energy_cross line 276
27. lemma OAI.WeakPinned.MinKernel.min_add_four line 286
28. lemma OAI.WeakPinned.MinKernel.energy_sum line 291
29. def OAI.WeakPinned.Hierarchy.Depth.outsideMass line 312
30. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_outside_product line 314
31. lemma OAI.WeakPinned.Hierarchy.Depth.outsideMass_square line 319
32. lemma OAI.WeakPinned.Hierarchy.Depth.iid_min_potential line 330
33. theorem OAI.WeakPinned.Hierarchy.Depth.iid_min_two_potentials line 339

    Source documentation

    The source min-potential upper bound before averaging places and grids.

    theorem iid_min_two_potentials (d' : Depth P) (hn : 2 ≤ Fintype.card P)
        (p : P → ℝ) (hp : ∀ x, 0≤p x) :
        (∑ x, ∑ y, p x*p y*min (d.potential x+d'.potential x) (d.potential y+d'.potential y)) ≤
          2*((∫ r, (d.outsideMass p r)^2)+(∫ r, (d'.outsideMass p r)^2)) := by
    …

    Mentions: OAI.WeakPinned.Hierarchy.Depth

34. lemma OAI.WeakPinned.Hierarchy.Depth.outsideMass_prob line 353
35. lemma OAI.WeakPinned.Hierarchy.Depth.outsideMass_zero line 361
36. lemma OAI.WeakPinned.Hierarchy.Depth.sumCells_nonneg line 364
37. lemma OAI.WeakPinned.Hierarchy.Depth.complement_le_sumCells line 368
38. lemma OAI.WeakPinned.Hierarchy.Depth.outside_square_bound line 376
39. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_outsideMass_square line 394
40. lemma OAI.WeakPinned.Hierarchy.Depth.integral_outsideMass line 400
41. theorem OAI.WeakPinned.Hierarchy.Depth.integrated_outside_square line 408

    Source documentation

    The integrable complement second moment estimate. All singleton terms are charged to the finite potential, not integrated as constant errors.

    theorem integrated_outside_square (hn : 2≤Fintype.card P)
        (w : I → ℝ) (B : I → Finset P) (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:ℝ)≤κ)
        (hdom : ∀ x, (∑ i, w i*prob (B i) x)≤M*prob Finset.univ x) :
        (∑ i, w i*(∫ r, (d.outsideMass (prob (B i)) r)^2)) ≤
          2*weightedIntegral d.mass (varianceCell w B T) +
          4*weightedIntegral d.mass (pairCell Finset.univ) +
          κ*M*(∑ x, prob Finset.univ x*d.potential x) := by
    …

    Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Hierarchy.Depth.M

42. lemma OAI.WeakPinned.MinKernel.energy_lower line 448

    Source documentation

    A fiber whose potential is a constant plus nonnegative overlap and a small signed grid error has a large iid minimum. This preserves self-pairs in the sampling, exactly as in the unbounded-scale argument.

    lemma energy_lower (p S L E : P → ℝ) (c : ℝ)
        (hp : ∀ x, 0≤p x) (hsum : (∑ x, p x)=1)
        (hL : ∀ x, 0≤L x)
        (hS : ∀ x, p x≠0 → S x=c+L x-E x) :
        (∑ x, p x*S x)-(∑ x, p x*L x)-(∑ x, p x*|E x|)≤energy p S S := by
    …

    Mentions: OAI.WeakPinned.MinKernel.energy

43. lemma OAI.WeakPinned.Hierarchy.Depth.min_upper_family line 483
44. lemma OAI.WeakPinned.Hierarchy.Depth.local_potential_fiber_bound line 508