OAI/Geometry/PinnedDistances/LogBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Bounded.logCost line 16
2. def OAI.WeakPinned.Bounded.logAverage line 19
3. lemma OAI.WeakPinned.Bounded.logCost_nonneg line 23
4. lemma OAI.WeakPinned.Bounded.logAverage_sum_bound line 26
5. lemma OAI.WeakPinned.Bounded.logAverage_nonneg line 33
6. lemma OAI.WeakPinned.Bounded.log_center line 39

   Source documentation

   One actual vertex serves as a tightness center: a row of the nonnegative distance-log matrix has at most the average row energy.

   lemma log_center (u : P → ℂ) (C : ℝ) (hn : 2 ≤ Fintype.card P) (hC : logAverage u ≤ C) :
       ∃ x : P, (∑ y, logCost u x y) ≤ C*(Fintype.card P : ℝ) := by
   …

   Mentions: OAI.WeakPinned.Bounded.logAverage, OAI.WeakPinned.Bounded.logCost

7. lemma OAI.WeakPinned.Bounded.log_cost_large line 52
8. lemma OAI.WeakPinned.Bounded.normalized_tail_card line 60

   Source documentation

   A normalized empirical tail bound from the average logarithmic cost.

   lemma normalized_tail_card (u : P → ℂ) (C : ℝ) (x : P)
       (hx : (∑ y, logCost u x y) ≤ C*(Fintype.card P : ℝ))
       (hn : 2 ≤ Fintype.card P) (R : ℝ) (hR : 1 < R) :
       ((Finset.univ.filter (fun y => R < ‖u y-u x‖)).card : ℝ)/(Fintype.card P : ℝ) ≤ C/Real.log R := by
   …

   Mentions: OAI.WeakPinned.Bounded.logCost

9. lemma OAI.WeakPinned.Bounded.log_cost_close line 81
10. lemma OAI.WeakPinned.Bounded.small_ball_card line 97

    Source documentation

    The true n^-1 diagonal term in the concentration estimate. The points may be arbitrarily close; injectivity is the only geometric condition.

    lemma small_ball_card (u : P → ℂ) (hu : Function.Injective u) (C : ℝ)
        (hn : 2 ≤ Fintype.card P) (hC : logAverage u ≤ C) (z : ℂ) (r : ℝ)
        (hr : 0<r) (hr2 : r<1/2) :
        (((Finset.univ.filter (fun x => ‖u x-z‖<r)).card : ℝ)/(Fintype.card P : ℝ))^2 ≤
          1/(Fintype.card P : ℝ)+C/(-Real.log (2*r)) := by
    …

    Mentions: OAI.WeakPinned.Bounded.logAverage

11. lemma OAI.WeakPinned.Bounded.weighted_deviation line 154
12. def OAI.WeakPinned.Bounded.pairMean line 176
13. lemma OAI.WeakPinned.Bounded.pairWeight_nonneg line 178
14. lemma OAI.WeakPinned.Bounded.pairMean_one line 185
15. lemma OAI.WeakPinned.Bounded.pairMean_mono line 190
16. lemma OAI.WeakPinned.Bounded.pairMean_add line 200
17. lemma OAI.WeakPinned.Bounded.pairMean_mul line 203
18. lemma OAI.WeakPinned.Bounded.pairMean_left line 207
19. lemma OAI.WeakPinned.Bounded.pairMean_right line 211
20. lemma OAI.WeakPinned.Bounded.pairMean_deviation line 216
21. lemma OAI.WeakPinned.Bounded.pairMean_overlap line 223
22. lemma OAI.WeakPinned.Bounded.depth_center_bound line 227
23. def OAI.WeakPinned.Bounded.singleScale line 249
24. lemma OAI.WeakPinned.Bounded.singleScale_nonneg line 252
25. lemma OAI.WeakPinned.Bounded.scaleEval_eq line 259
26. lemma OAI.WeakPinned.Bounded.singleScale_le_left line 262
27. lemma OAI.WeakPinned.Bounded.singleScale_le_right line 265
28. def OAI.WeakPinned.Bounded.rawDepth line 268
29. def OAI.WeakPinned.Bounded.pairGridError line 269
30. lemma OAI.WeakPinned.Bounded.raw_center_grid_bound line 272
31. lemma OAI.WeakPinned.Bounded.pairGridError_integrable line 293
32. lemma OAI.WeakPinned.Bounded.mean_pairGridError line 304
33. lemma OAI.WeakPinned.Bounded.arch_log_center_bound line 332
34. def OAI.WeakPinned.Bounded.logNormalize line 361
35. lemma OAI.WeakPinned.Bounded.logNormalize_injective line 363
36. lemma OAI.WeakPinned.Bounded.logAverage_pairMean line 369
37. lemma OAI.WeakPinned.Bounded.logNormalize_log line 379
38. lemma OAI.WeakPinned.Bounded.logNormalize_bound line 386
39. lemma OAI.WeakPinned.Bounded.logAverage_translate line 398