OAI/Geometry/PinnedDistances/Variance.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPinned.Variance.prob line 30
  2. def OAI.WeakPinned.Variance.pairProb line 32
  3. def OAI.WeakPinned.Variance.mixedProb line 37

    Source documentation

    Mixed cell probability, including B=P without an undefined outside branch. The outside column formula is never used when B=P.

    def mixedProb (B : Finset P) (x y : P) : ℝ :=
…

    Mentions: OAI.WeakPinned.B

  4. lemma OAI.WeakPinned.Variance.sum_prob line 43
  5. lemma OAI.WeakPinned.Variance.sum_pairProb line 48
  6. lemma OAI.WeakPinned.Variance.pairProb_symm line 70
  7. lemma OAI.WeakPinned.Variance.pairProb_diag line 74
  8. lemma OAI.WeakPinned.Variance.ambient_card_ge_two line 78
  9. lemma OAI.WeakPinned.Variance.mixedProb_decompose line 81
  10. lemma OAI.WeakPinned.Variance.sum_mixedProb line 94
  11. lemma OAI.WeakPinned.Variance.sum_mixedProb_left line 111
  12. lemma OAI.WeakPinned.Variance.mixedProb_diag line 121
  13. def OAI.WeakPinned.Variance.signedPair line 124
  14. lemma OAI.WeakPinned.Variance.signedPair_diag line 127
  15. lemma OAI.WeakPinned.Variance.signedPair_row line 130
  16. lemma OAI.WeakPinned.Variance.signedPair_col line 139
  17. lemma OAI.WeakPinned.Variance.additive_cancel line 151

    Source documentation

    Exact cancellation against every additive off-diagonal overlap kernel. Only the sum of the two marginals is constrained.

    lemma additive_cancel (H L : P → P → ℝ) (b : ℝ) (S : P → ℝ)
    (hdiag : ∀ x, H x x = 0)
    (hmass : (∑ x, ∑ y, H x y) = 0)
    (hmarg : ∀ x, (∑ y, H x y) + ∑ y, H y x = 0)
    (hL : ∀ x y, x ≠ y → L x y = b + S x + S y) :
    (∑ x, ∑ y, H x y * L x y) = 0 := by
…
  18. lemma OAI.WeakPinned.Variance.variance_cancel line 175
  19. def OAI.WeakPinned.Variance.pairCell line 190

    Source documentation

    Exact cell probabilities, with the diagonal excluded.

    def pairCell (B C : Finset P) : ℝ := ∑ x ∈ C, ∑ y ∈ C, pairProb B x y

    Mentions: OAI.WeakPinned.B, OAI.WeakPinned.Variance.pairProb

  20. def OAI.WeakPinned.Variance.mixedCell line 192
  21. def OAI.WeakPinned.Variance.cellProb line 194
  22. lemma OAI.WeakPinned.Variance.sum_prob_cell line 197
  23. lemma OAI.WeakPinned.Variance.pairCell_formula line 202
  24. lemma OAI.WeakPinned.Variance.sum_outside_cell line 222
  25. lemma OAI.WeakPinned.Variance.mixedCell_formula line 233
  26. lemma OAI.WeakPinned.Variance.cellProb_nonneg line 242
  27. lemma OAI.WeakPinned.Variance.cellProb_le_one line 247
  28. lemma OAI.WeakPinned.Variance.pairCell_nonneg line 254
  29. lemma OAI.WeakPinned.Variance.pair_fraction line 267
  30. lemma OAI.WeakPinned.Variance.pairCell_centered line 273
  31. lemma OAI.WeakPinned.Variance.mixedCell_centered line 282
  32. lemma OAI.WeakPinned.Variance.mixedCell_le_product line 292
  33. lemma OAI.WeakPinned.Variance.signedCell_formula line 304
  34. lemma OAI.WeakPinned.Variance.pair_fraction_bounds line 319
  35. lemma OAI.WeakPinned.Variance.uniform_pair_comparison line 340
  36. lemma OAI.WeakPinned.Variance.fiber_pair_lower line 350
  37. lemma OAI.WeakPinned.Variance.singleton_pairCell line 363
  38. lemma OAI.WeakPinned.Variance.singleton_mixedCell line 373
  39. lemma OAI.WeakPinned.Variance.singleton_fiber_term line 384
  40. def OAI.WeakPinned.Variance.signedCell line 393
  41. lemma OAI.WeakPinned.Variance.signedCell_eq line 396
  42. lemma OAI.WeakPinned.Variance.singleton_signedCell line 401
  43. lemma OAI.WeakPinned.Variance.correction_bound line 404
  44. lemma OAI.WeakPinned.Variance.signedCell_lower line 419

    Source documentation

    The finite large-cell estimate before converting a to pair mass.

    lemma signedCell_lower (B C : Finset P) (hB : 2 ≤ B.card) (ε : ℝ)
    (hk : 1 / ((B.card : ℝ)-1) ≤ ε)
    (hn : 1 / ((Fintype.card P : ℝ)-1) ≤ ε) :
    (cellProb B C - cellProb Finset.univ C)^2 -
      ε * (cellProb B C + cellProb Finset.univ C) ≤ signedCell B C := by
…

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

  45. lemma OAI.WeakPinned.Variance.mean_cell_bound line 438
  46. lemma OAI.WeakPinned.Variance.family_large_raw line 445
  47. lemma OAI.WeakPinned.Variance.family_large line 474
  48. lemma OAI.WeakPinned.Variance.family_small line 495
  49. lemma OAI.WeakPinned.Variance.zero_uniform_pair_iff line 532

    Source documentation

    Zero pair overlap is precisely an empty or singleton occurrence.

    lemma zero_uniform_pair_iff (C : Finset P) :
    pairCell Finset.univ C = 0 ↔ C.card ≤ 1 := by
…

    Mentions: OAI.WeakPinned.Variance.pairCell

  50. lemma OAI.WeakPinned.Variance.finite_weighted_bound line 555
  51. lemma OAI.WeakPinned.Variance.integrable_cell_function line 572

    Source documentation

    The only integrability input needed for any fixed finite cell function vanishing on singletons is integrability of the off-diagonal pair mass.

    lemma integrable_cell_function (C : Ω → Finset P) (μ : Measure Ω)
    (hC : Measurable C) (hq : Integrable (fun ω => pairCell Finset.univ (C ω)) μ)
    (f : Finset P → ℝ) (hf : ∀ D, D.card ≤ 1 → f D = 0) :
    Integrable (fun ω => f (C ω)) μ := by
…

    Mentions: OAI.WeakPinned.Variance.pairCell

  52. def OAI.WeakPinned.Variance.offDiagonalCell line 581
  53. lemma OAI.WeakPinned.Variance.offDiagonalCell_singleton line 585
  54. def OAI.WeakPinned.Variance.overlap line 592
  55. lemma OAI.WeakPinned.Variance.cell_sum_eq line 595
  56. lemma OAI.WeakPinned.Variance.integral_signedCell line 604
  57. lemma OAI.WeakPinned.Variance.integrated_cancel line 624
  58. def OAI.WeakPinned.Variance.varianceCell line 636
  59. lemma OAI.WeakPinned.Variance.varianceCell_singleton line 642
  60. lemma OAI.WeakPinned.Variance.varianceCell_bound line 648
  61. theorem OAI.WeakPinned.Variance.integrated_variance line 687

    Source documentation

    The integrated off-diagonal variance estimate before specializing the threshold and denominator errors to powers of n. The pair overlap may have infinite singleton tails; no diagonal integral is used.

    theorem integrated_variance (C : Ω → Finset P) (μ : Measure Ω)
    (hC : Measurable C) (hq : Integrable (fun ω => pairCell Finset.univ (C ω)) μ)
    (b : ℝ) (S : P → ℝ)
    (hL : ∀ x y, x ≠ y → overlap C μ x y = b + S x + S y)
    (w : I → ℝ) (B : I → Finset P) (T M ε τ : ℝ)
    (hw : ∀ i, 0 ≤ w i) (hW : (∑ i, w i) ≤ 1)
    (hT : 1 ≤ T) (hM : 0 ≤ M) (hε : 0 ≤ ε) (hτ : 0 < τ)
    (hscale : τ * Fintype.card P ≤ T)
    (hB : ∀ i, 2 ≤ (B i).card)
    (hk : ∀ i, 1 / (((B i).card : ℝ)-1) ≤ ε)
    (hn : 1 / ((Fintype.card P : ℝ)-1) ≤ ε)
    (hdom : ∀ x, (∑ i, w i * prob (B i) x) ≤ M * prob Finset.univ x) :
…

    Mentions: OAI.WeakPinned.Variance.pairCell, OAI.WeakPinned.Variance.overlap, OAI.WeakPinned.B, OAI.WeakPinned.Variance.prob