OAI/Geometry/PinnedDistances/WeightedSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Bounded.weighted_select line 15

   Source documentation

   Simultaneous selection from a normalized weighted family. In particular, there is no required lower bound on a nonzero archimedean-place weight.

   lemma weighted_select {J : Type u1} [Fintype J] (w T V : J → ℝ) (C ε : ℝ)
       (hw : ∀ j, 0 < w j) (hW : ∑ j, w j = 1)
       (hT : ∀ j, 0 ≤ T j) (hV : ∀ j, 0 ≤ V j)
       (hC : 0 ≤ C) (hε : 0 < ε)
       (hTC : ∑ j, w j * T j ≤ C) (hVE : ∑ j, w j * V j ≤ ε) :
       ∃ j, T j ≤ 2*C+1 ∧ V j ≤ 2*ε := by
   …

2. lemma OAI.WeakPinned.Bounded.massEval_nonneg line 54
3. def OAI.WeakPinned.Bounded.scaleEval line 60
4. lemma OAI.WeakPinned.Bounded.scaleEval_nonneg line 64
5. lemma OAI.WeakPinned.Bounded.integrable_scaleEval line 73
6. lemma OAI.WeakPinned.Bounded.average_scaleEval line 79
7. def OAI.WeakPinned.Bounded.archMean line 87
8. lemma OAI.WeakPinned.Bounded.archMean_nonneg line 91
9. lemma OAI.WeakPinned.Bounded.archMean_le_average line 94
10. lemma OAI.WeakPinned.Bounded.archWeight_pos line 100
11. lemma OAI.WeakPinned.Bounded.select_arch line 108

    Source documentation

    Both the local scale and any nonnegative sum of variance cells are controlled at one genuine complex embedding.

    lemma select_arch (hn : 2≤Fintype.card P) (q : Finset P → ℝ) (hq : ∀ C, 0≤q C)
        (C ε : ℝ) (hC : 0≤C) (hε : 0<ε)
        (hscale : overlapScale Z₁ Z₂ h₁ h₂ + potentialScale Z₁ Z₂ h₁ h₂ ≤ C)
        (hvar : weightedIntegral (totalMass Z₁ Z₂ h₁ h₂) q ≤ ε) :
        ∃ v : InfinitePlace K,
          archMean Z₁ Z₂ scaleEval v ≤ 2*C+1 ∧ archMean Z₁ Z₂ (massEval q) v ≤ 2*ε := by
    …

    Mentions: OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale, OAI.WeakPinned.Bounded.archMean, OAI.WeakPinned.Bounded.scaleEval