OAI/Probability/Ising/Influence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BufferedIsing.DSS.tanh_nonneg_of_nonneg line 15
2. lemma OAI.BufferedIsing.DSS.reference_update line 20
3. lemma OAI.BufferedIsing.DSS.update_neg line 26
4. lemma OAI.BufferedIsing.DSS.mixture_weight_range line 30
5. lemma OAI.BufferedIsing.DSS.influence_step line 39

   Source documentation

   The induction step combines bounds for a smaller increment support and for pinned gaps.

   lemma influence_step (J : V → V → ℝ) (hJ : ∀ u v, 0 ≤ J u v)
       (g h : V → ℝ) (hh : 0 ≤ h) (v o : V) (t : ℝ) (ht : 0 ≤ t)
       (Hfield : ∀ (g' : V → ℝ) (o' : V),
         mean J (g' + h) o' - mean J (g' - h) o' ≤ mean J h o' - mean J (-h) o')
       (Hpin : pinMean J (g + h) v true o - pinMean J (g - h) v false o ≤
         pinMean J h v true o - pinMean J (-h) v false o) :
       mean J ((g + h) + fieldAt v t) o - mean J ((g - h) + fieldAt v (-t)) o ≤
         mean J (h + fieldAt v t) o - mean J ((-h) + fieldAt v (-t)) o := by
   …

   Mentions: OAI.BufferedIsing.DSS.mean, OAI.BufferedIsing.DSS.pinMean, OAI.BufferedIsing.DSS.fieldAt

6. def OAI.BufferedIsing.DSS.InfluenceBound line 116

   Source documentation

   The nonnegative-increment influence bound for a fixed finite coupling array.

   def InfluenceBound (J : V → V → ℝ) : Prop :=
   …

7. lemma OAI.BufferedIsing.DSS.pin_comparison_of_removed line 120
8. def OAI.BufferedIsing.DSS.positiveSupport line 153
9. theorem OAI.BufferedIsing.DSS.influence_of_card line 156

   Source documentation

   The influence inequality follows by induction on the vertex count and the positive-increment support size.

   theorem influence_of_card (n : ℕ) :
       ∀ (V : Type u) [Fintype V], Fintype.card V = n →
         ∀ (J : V → V → ℝ), (∀ u v, 0 ≤ J u v) → InfluenceBound J := by
   …

   Mentions: OAI.BufferedIsing.DSS.InfluenceBound

10. theorem OAI.BufferedIsing.DSS.influence line 221

    Source documentation

    Arbitrary real background fields do not increase the influence of a finite nonnegative perturbation, on every finite ferromagnetic graph.

    theorem influence (J : V → V → ℝ) (hJ : ∀ u v, 0 ≤ J u v) : InfluenceBound J :=
    …

    Mentions: OAI.BufferedIsing.DSS.InfluenceBound

11. lemma OAI.BufferedIsing.DSS.pin_gap_comparison line 224
12. def OAI.BufferedIsing.DSS.correlation line 232
13. lemma OAI.BufferedIsing.DSS.sum_pin_first line 235
14. lemma OAI.BufferedIsing.DSS.correlation_split line 242
15. lemma OAI.BufferedIsing.DSS.covariance_identity line 251
16. theorem OAI.BufferedIsing.DSS.covariance_le_zero_field line 261

    Source documentation

    Conditioning at a site and applying the influence inequality bounds arbitrary-field covariance by zero-field correlation.

    theorem covariance_le_zero_field (J : V → V → ℝ) (hJ : ∀ u v, 0 ≤ J u v)
        (g : V → ℝ) (u v : V) :
        correlation J g u v - mean J g u * mean J g v ≤ correlation J 0 u v := by
    …

    Mentions: OAI.BufferedIsing.DSS.correlation, OAI.BufferedIsing.DSS.mean