OAI/Probability/InvariantIsing/Cavity/CavityQuadraticReplica.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.cavityQuadratic_terminalGibbsLaw line 15
2. theorem OAI.InvariantIsing.cavity_innovation_replica_law line 35
3. theorem OAI.InvariantIsing.cavity_quadratic_replica_innovation_law line 77
4. theorem OAI.InvariantIsing.cavity_innovation_mark_path_law line 116

   Source documentation

   The entire sampled innovation path has the independent-mark cascade law, with the common-prefix dependence carried only by the sampled leaves.

   theorem cavity_innovation_mark_path_law {d : ℕ} (n : ℕ) (b : ℕ → ℝ)
       (hb : CascadeExponents 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 (EuclideanSpace ℝ (Fin d))).withDensity
         (fun a => ENNReal.ofReal (c i (s, a) ^ b i))).map (fun a => g i (s, a))) =
           (ν i : Measure (EuclideanSpace ℝ (Fin d)))) (s : EuclideanSpace ℝ (Fin d)) :
       ((probabilityReplicaKernel (noiseTiltedLeafLaw n c (fun _ p => p.1 + p.2) s)
         (measurable_noiseTiltedLeafLaw n hc (fun _ => measurable_fst.add measurable_snd) s)) ∘ₘ
   …