OAI/Probability/Ising/Covariance.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BufferedIsing.tableCovariance line 10

   Source documentation

   Covariance of the two canonical spins of a positive two-spin table.

   noncomputable def tableCovariance (w : Bool → Bool → ℝ) : ℝ :=
   …

2. def OAI.BufferedIsing.tiltTable line 16

   Source documentation

   Multiplying by terminal fields does not change the effective interaction.

   noncomputable def tiltTable (w : Bool → Bool → ℝ) (A B : ℝ) (s t : Bool) : ℝ :=
   …

3. lemma OAI.BufferedIsing.tableCoupling_tilt line 19
4. lemma OAI.BufferedIsing.tableCovariance_formula line 25
5. lemma OAI.BufferedIsing.balancedTable_partition_le line 34
6. lemma OAI.BufferedIsing.tableCovariance_le_balanced line 51
7. lemma OAI.BufferedIsing.tableCovariance_le_tanh line 84
8. def OAI.BufferedIsing.addTerminalFields line 93

   Source documentation

   Actual addition of two (possibly mixed-sign) finite external fields.

   def addTerminalFields {n : ℕ} (h : Fin n → ℝ) (u v : Fin n) (A B : ℝ)
       (x : Fin n) : ℝ := h x + (if x = u then A else 0) + (if x = v then B else 0)

9. lemma OAI.BufferedIsing.energy_addTerminalFields line 96
10. lemma OAI.BufferedIsing.weight_addTerminalFields line 103
11. lemma OAI.BufferedIsing.pairTable_addTerminalFields line 112
12. lemma OAI.BufferedIsing.pairTable_weight_pos line 125
13. lemma OAI.BufferedIsing.pairTable_weight_eq_jointWeight line 139
14. lemma OAI.BufferedIsing.pairTable_weight_det_nonneg line 146
15. lemma OAI.BufferedIsing.pairTable_weight_covariance line 159
16. lemma OAI.BufferedIsing.pairTable_balancedGraph line 167

    Source documentation

    Balancing a marginal is realized by external fields on the SAME graph.

    lemma pairTable_balancedGraph {n m : ℕ} (G : FiniteGraph n m)
        (h : Fin n → ℝ) (u v : Fin n) :
        pairTable (weight G (addTerminalFields h u v
          (-tableFieldLeft (pairTable (weight G h) u v))
          (-tableFieldRight (pairTable (weight G h) u v)))) u v =
          balancedTable (pairTable (weight G h) u v) := by
    …

    Mentions: OAI.BufferedIsing.FiniteGraph, OAI.BufferedIsing.pairTable, OAI.BufferedIsing.weight, OAI.BufferedIsing.addTerminalFields, OAI.BufferedIsing.tableFieldLeft, OAI.BufferedIsing.tableFieldRight, OAI.BufferedIsing.balancedTable

17. lemma OAI.BufferedIsing.weight_zero_spinFlip line 177
18. lemma OAI.BufferedIsing.zero_pairTable_correlation line 182
19. lemma OAI.BufferedIsing.tanh_le_tanh_iff line 190
20. def OAI.BufferedIsing.EffectiveCouplingBound line 197

    Source documentation

    External fields do not increase the two-terminal effective coupling.

    def EffectiveCouplingBound : Prop :=
    …

21. lemma OAI.BufferedIsing.expectation_one line 202
22. theorem OAI.BufferedIsing.covarianceBound_iff_effectiveCouplingBound line 210

    Source documentation

    For finite ferromagnetic graphs, the arbitrary-field covariance bound and zero-field maximality of the effective coupling are equivalent.

    theorem covarianceBound_iff_effectiveCouplingBound :
        ArbitraryFieldCovarianceBound ↔ EffectiveCouplingBound := by
    …

    Mentions: OAI.BufferedIsing.ArbitraryFieldCovarianceBound, OAI.BufferedIsing.EffectiveCouplingBound