OAI/Probability/InvariantIsing/Cavity/CavityResidualInnovation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The joint innovation map for a true cascade leaf and its ordinary terminal residual. All residual randomness remains outside the cascade.

  1. def OAI.InvariantIsing.cavityQuadraticResidualGibbs line 14
  2. instance OAI.InvariantIsing.cavityQuadraticResidualGibbs_probability line 23
  3. lemma OAI.InvariantIsing.measurable_cavityQuadraticResidualGibbs line 29
  4. def OAI.InvariantIsing.cavityResidualInnovationMap line 50
  5. lemma OAI.InvariantIsing.measurable_cavityResidualInnovationMap line 61
  6. theorem OAI.InvariantIsing.cavity_residual_innovation_leaf_law line 82

    Source documentation

    At every regular tree the transformed leaf and centered terminal residual are independent, with the leaf law of the innovation tree.

    theorem cavity_residual_innovation_leaf_law {d : ℕ} (n : ℕ)
    (K : Matrix (Fin d) (Fin d) ℝ) (H S : ℕ → Matrix (Fin d) (Fin d) ℝ) (b : ℕ → ℝ)
    (hK : K.transpose = K) (hR : (H n).PosSemidef)
    (hdet : IsUnit (1 - H n * K).det)
    (hQ : (cavityFactorPrecision K (CFC.sqrt (H n))).PosDef)
    (s : EuclideanSpace ℝ (Fin d)) (V : NoiseTree (EuclideanSpace ℝ (Fin d)) n)
    (hZ : cavityResidualPartition n K (H n) s V < ∞)
    (hV : NoiseGibbsRegular n b (cavityGaussianMarks S)
      (fun i => cavityQuadraticStepWeight K (H i) (H (i + 1)) (b i))
      (fun _ p => p.1 + p.2) s V) :
    (cavityQuadraticResidualGibbs n K (H n) s V).map
      (fun p => (cavityInnovationLeaf n
…

    Mentions: OAI.InvariantIsing.cavityFactorPrecision, OAI.InvariantIsing.cavityResidualPartition, OAI.InvariantIsing.cavityGaussianMarks, OAI.InvariantIsing.cavityQuadraticStepWeight, OAI.InvariantIsing.cavityQuadraticResidualGibbs, OAI.InvariantIsing.cavityInnovationLeaf