CavityInnovationTree.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-depth retained Gaussian innovation construction. The intensity calculation only requires the normalized conditional fractional moment, not an ordinary exponential moment of a terminal.

lemma OAI.InvariantIsing.cavity_map_powerIntensity_innovation line 16

def OAI.InvariantIsing.cavityInnovationTree line 92

Source documentation

Retain and rescale each Gaussian mark while updating the running sum by the original increment.

def cavityInnovationTree {d : ℕ} : (n : ℕ) → (ℕ → ℝ) →
    (ℕ → ProbabilityMeasure (EuclideanSpace ℝ (Fin d))) →
    (ℕ → EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) → ℝ) →
    (ℕ → EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) →
    EuclideanSpace ℝ (Fin d) → NoiseTree (EuclideanSpace ℝ (Fin d)) n →
      NoiseTree (EuclideanSpace ℝ (Fin d)) n
  | 0, _, _, _, _, _, _ => PUnit.unit
  | n + 1, b, μ, c, g, s, T =>
      (sigmaPart ((powerIntensity (b 0)).prod ((μ 0 : Measure _).prod
        (noiseCascadeLaw (EuclideanSpace ℝ (Fin d)) n (fun j => b (j + 1))
          (fun j => μ (j + 1))))) T).map
        (fun p => (c 0 (s, p.2.1) * p.1, (g 0 (s, p.2.1),
…

lemma OAI.InvariantIsing.measurable_cavityInnovationTree line 107

theorem OAI.InvariantIsing.cavityInnovationTree_law line 132

Source documentation

If the retained innovation has the same law at every ancestor, the full transformed tree has independent marks with that law.

theorem cavityInnovationTree_law {d : ℕ} (n : ℕ) (b : ℕ → ℝ)
    (μ ν : ℕ → ProbabilityMeasure (EuclideanSpace ℝ (Fin d)))
    (c : ℕ → EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) → ℝ)
    (g : ℕ → EuclideanSpace ℝ (Fin d) × EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d))
    (hc : ∀ i, Measurable (c i)) (hg : ∀ i, Measurable (g i))
    (hcpos : ∀ i s a, 0 < c i (s, a))
    (hν : ∀ i s, (((μ i : Measure _).withDensity
      (fun a => ENNReal.ofReal (c i (s, a) ^ b i))).map (fun a => g i (s, a))) =
        (ν i : Measure _)) (s : EuclideanSpace ℝ (Fin d)) :
    (noiseCascadeLaw (EuclideanSpace ℝ (Fin d)) n b μ : Measure _).map
      (cavityInnovationTree n b μ c g s) = noiseCascadeLaw (EuclideanSpace ℝ (Fin d)) n b ν := by
…

Mentions: OAI.InvariantIsing.cavityInnovationTree