OAI/Geometry/PinnedDistances/ArithmeticVariance.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Global.cellMass line 30
2. lemma OAI.WeakPinned.Global.cellMass_nonneg line 34
3. lemma OAI.WeakPinned.Global.cellMass_singleton line 40
4. lemma OAI.WeakPinned.Global.cellMass_overlap line 43
5. def OAI.WeakPinned.Variance.weightedIntegral line 67

   Source documentation

   Finite linear model of the actual occurrence integral on expressions vanishing on singleton and empty cells. Multiplicities are in m.

   def weightedIntegral (m : Finset P → ℝ) (f : Finset P → ℝ) : ℝ := ∑ C, m C * f C

6. def OAI.WeakPinned.Variance.weightedOverlap line 69
7. lemma OAI.WeakPinned.Variance.weighted_cancel line 72
8. lemma OAI.WeakPinned.Variance.weighted_variance line 97
9. def OAI.WeakPinned.Global.totalMass line 152
10. def OAI.WeakPinned.Global.totalPotential line 154
11. def OAI.WeakPinned.Global.baseConstant line 156
12. lemma OAI.WeakPinned.Global.totalMass_nonneg line 158
13. lemma OAI.WeakPinned.Global.totalPotential_nonneg line 161
14. lemma OAI.WeakPinned.Global.totalMass_overlap line 164
15. theorem OAI.WeakPinned.Global.arithmetic_variance line 176

    Source documentation

    Unconditional arithmetic-hierarchy instance of the quantitative variance bound. The overlap identity follows from the product formula, and the family hypotheses are exactly finite sampling data.

    theorem arithmetic_variance {I : Type u7} [Fintype I]
        (hnP : 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) (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) :
        weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (varianceCell w B T) ≤
          (2*ε*(M₀+1)/τ)*weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) (pairCell Finset.univ) +
    …

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