OAI/Probability/InvariantIsing/Cavity/CavityQuadraticTree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independent Gaussian innovations for the retained finite quadratic tree.

  1. def OAI.InvariantIsing.cavityGaussianMarks line 14
  2. def OAI.InvariantIsing.cavityStepInnovation line 18
  3. lemma OAI.InvariantIsing.measurable_cavityStepInnovation line 24
  4. theorem OAI.InvariantIsing.cavity_quadratic_innovation_tree_law line 32

    Source documentation

    Actual backward quadratic weights turn the finite Gaussian tree into a tree with independent centered Gaussian innovations.

    theorem cavity_quadratic_innovation_tree_law {d : ℕ} (n : ℕ)
    (K : Matrix (Fin d) (Fin d) ℝ)
    (H S : ℕ → Matrix (Fin d) (Fin d) ℝ) (b : ℕ → ℝ)
    (hK : K.transpose = K) (hH : ∀ i, (H i).transpose = H i)
    (hS : ∀ i, (S i).PosSemidef) (hb : ∀ i, 0 < b i)
    (hdet : ∀ i, IsUnit (1 - H i * K).det)
    (hΔ : ∀ i, H i - H (i + 1) = b i • S i)
    (hQ : ∀ i, (cavityFactorPrecision
      (b i • cavityBackwardQuadratic K (H (i + 1))) (CFC.sqrt (S i))).PosDef)
    (u : EuclideanSpace ℝ (Fin d)) :
    (noiseCascadeLaw (EuclideanSpace ℝ (Fin d)) n b (cavityGaussianMarks S) : Measure _).map
      (cavityInnovationTree n b (cavityGaussianMarks S)
…

    Mentions: OAI.InvariantIsing.cavityFactorPrecision, OAI.InvariantIsing.cavityBackwardQuadratic, OAI.InvariantIsing.cavityGaussianMarks, OAI.InvariantIsing.cavityInnovationTree