OAI/Probability/Ising/Marginals.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BufferedIsing.jointWeight_logSupermodular line 10

   Source documentation

   The four functions theorem preserves log-supermodularity under marginalization.

   lemma jointWeight_logSupermodular {n m : ℕ} (G : FiniteGraph n m)
       (h : Fin n → ℝ) (I J F : Finset (Fin n)) (τ a a' b b' : Spins n) :
       jointWeight G h I J F τ a b * jointWeight G h I J F τ a' b' ≤
         jointWeight G h I J F τ (a ⊓ a') (b ⊓ b') *
         jointWeight G h I J F τ (a ⊔ a') (b ⊔ b') := by
   …

   Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins, OAI.BufferedIsing.jointWeight

2. lemma OAI.BufferedIsing.extreme_rectangle line 58

   Source documentation

   The extreme-rectangle bound does not require the four configurations to be ordered.

   lemma extreme_rectangle {A B : Type*} [PartialOrder A] [BoundedOrder A]
       [PartialOrder B] [BoundedOrder B] (f : A → B → ℝ)
       (hrect : ∀ u v s t, u ≤ v → s ≤ t → f u t + f v s ≤ f u s + f v t)
       (a a' : A) (b b' : B) :
       |f a b + f a' b' - f a b' - f a' b| ≤
         f ⊤ ⊤ + f ⊥ ⊥ - f ⊤ ⊥ - f ⊥ ⊤ := by
   …

3. lemma OAI.BufferedIsing.marginal_extreme_rectangle line 78

   Source documentation

   The extreme-rectangle bound for the arbitrary-field Ising marginal with common pins.

   lemma marginal_extreme_rectangle {n m : ℕ} (G : FiniteGraph n m)
       (h : Fin n → ℝ) (I J F : Finset (Fin n))
       (hIJ : Disjoint I J) (hIF : Disjoint I F) (hJF : Disjoint J F)
       (τ a a' b b' : Spins n) :
       |Real.log (jointWeight G h I J F τ a b) +
           Real.log (jointWeight G h I J F τ a' b') -
           Real.log (jointWeight G h I J F τ a b') -
           Real.log (jointWeight G h I J F τ a' b)| ≤
         Real.log (jointWeight G h I J F τ ⊤ ⊤) +
           Real.log (jointWeight G h I J F τ ⊥ ⊥) -
           Real.log (jointWeight G h I J F τ ⊤ ⊥) -
           Real.log (jointWeight G h I J F τ ⊥ ⊤) := by
   …

   Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins, OAI.BufferedIsing.jointWeight

4. lemma OAI.BufferedIsing.normalized_ratio_of_rectangles line 102

   Source documentation

   A general normalization lemma. Rectangle control on unnormalized positive weights bounds the ACTUAL normalized pointwise ratio, not merely its odds.

   lemma normalized_ratio_of_rectangles {A B : Type*} [Fintype A]
       (p : A → B → ℝ) (hp : ∀ a b, 0 < p a b) (L : ℝ)
       (hrect : ∀ a a' b b',
         |Real.log (p a b) + Real.log (p a' b') - Real.log (p a b') -
           Real.log (p a' b)| ≤ L) (a : A) (b b' : B) :
       Real.exp (-L) ≤ (p a b / ∑ x, p x b) / (p a b' / ∑ x, p x b') ∧
         (p a b / ∑ x, p x b) / (p a b' / ∑ x, p x b') ≤ Real.exp L := by
   …

5. def OAI.BufferedIsing.restrictSpin line 143
6. def OAI.BufferedIsing.extendSpin line 145
7. lemma OAI.BufferedIsing.restrict_extend line 148
8. lemma OAI.BufferedIsing.agreesOn_iff_restrict_eq line 153
9. lemma OAI.BufferedIsing.jointWeight_extend_restrict line 162
10. lemma OAI.BufferedIsing.sum_jointWeight_eq_denominator line 168
11. def OAI.BufferedIsing.extremeLogOdds line 183
12. lemma OAI.BufferedIsing.conditional_ratio_extreme line 191

    Source documentation

    The normalized conditional probability ratio is bounded by the extreme log odds.

    lemma conditional_ratio_extreme {n m : ℕ} (G : FiniteGraph n m)
        (h : Fin n → ℝ) (I J F : Finset (Fin n))
        (hIJ : Disjoint I J) (hIF : Disjoint I F) (hJF : Disjoint J F)
        (τ a b b' : Spins n) :
        Real.exp (-extremeLogOdds G h I J F τ) ≤
            conditionalProb G h I J F a b τ / conditionalProb G h I J F a b' τ ∧
          conditionalProb G h I J F a b τ / conditionalProb G h I J F a b' τ ≤
            Real.exp (extremeLogOdds G h I J F τ) := by
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.Spins, OAI.BufferedIsing.extremeLogOdds, OAI.BufferedIsing.conditionalProb

13. lemma OAI.BufferedIsing.conditionalProb_pos line 209
14. lemma OAI.BufferedIsing.positive_average line 222
15. lemma OAI.BufferedIsing.mixture_ratio_of_pointwise line 237

    Source documentation

    Multiplicative pointwise control survives arbitrary mixtures on both sides. The proof uses the original constants without a second loss.

    lemma mixture_ratio_of_pointwise {B : Type*} [Fintype B]
        (p : B → ℝ) (hp : ∀ b, 0 < p b) (L U : ℝ)
        (hbound : ∀ b b', L ≤ p b / p b' ∧ p b / p b' ≤ U)
        (μ ν : B → ℝ) (hμ : ∀ b, 0 ≤ μ b) (hν : ∀ b, 0 ≤ ν b)
        (hμsum : ∑ b, μ b = 1) (hνsum : ∑ b, ν b = 1) :
        L ≤ (∑ b, μ b * p b) / (∑ b, ν b * p b) ∧
          (∑ b, μ b * p b) / (∑ b, ν b * p b) ≤ U := by
    …

16. lemma OAI.BufferedIsing.mixture_ratio_extreme line 273
17. lemma OAI.BufferedIsing.extremeLogOdds_nonneg line 289