OAI/Probability/InvariantIsing/Cavity/CavityInnovationLeaves.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Leaf transport for the retained quadratic innovation tree.

  1. def OAI.InvariantIsing.cavityInnovationLeaf line 13
  2. lemma OAI.InvariantIsing.measurable_cavityInnovationLeaf line 23
  3. lemma OAI.InvariantIsing.cavityInnovationTree_forget line 37
  4. lemma OAI.InvariantIsing.cavityInnovationTree_total line 83
  5. def OAI.InvariantIsing.cavityLeafSum line 94
  6. theorem OAI.InvariantIsing.cavityInnovationLeaf_sum line 100

    Source documentation

    The transformed increments telescope to the rescaled final sum.

    theorem cavityInnovationLeaf_sum {d : ℕ} (n : ℕ)
    (K : Matrix (Fin d) (Fin d) ℝ) (H : ℕ → Matrix (Fin d) (Fin d) ℝ)
    (c : ℕ → EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) → ℝ)
    (s : EuclideanSpace ℝ (Fin d)) (v : NoiseLeaf (EuclideanSpace ℝ (Fin d)) n) :
    cavityLeafSum n (Matrix.toEuclideanCLM (𝕜 := ℝ) (1 - H 0 * K)⁻¹ s)
…

    Mentions: OAI.InvariantIsing.cavityLeafSum

  7. theorem OAI.InvariantIsing.cavityInnovationLeaf_terminal_sum line 119