OAI/Probability/InvariantIsing/Fields/CascadeMarking.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite-depth Gaussian marking input used in the one-site functional. The logarithmic terminal is unbounded; the linear-growth cascade theorem supplies its integrability. This is the Gaussian specialization of Bolthausen--Sznitman (1998), Appendix Proposition A.2.

  1. lemma OAI.InvariantIsing.integral_gaussianReal_zero_eq_standard line 20
  2. lemma OAI.InvariantIsing.gaussianOperator_eq_gaussian_logMean line 36
  3. lemma OAI.InvariantIsing.gaussianCascadeRecursion_eq_fold line 46
  4. def OAI.InvariantIsing.gaussianCascadeLaw line 74
  5. def OAI.InvariantIsing.gaussianCascadeLog line 79
  6. theorem OAI.InvariantIsing.gaussianCascadeLog_recursion line 86

    Source documentation

    Exact finite Gaussian marking recursion, with the integrability needed to take the outer expectation. No boundedness of log cosh is assumed.

    theorem gaussianCascadeLog_recursion (n : ℕ) (b : ℕ → ℝ) (v : ℕ → ℝ≥0)
    (hb : IsingPerceptron.CascadeExponents n b) (x : ℝ) :
    Integrable (gaussianCascadeLog n x) (gaussianCascadeLaw n b v) ∧
      (∫ T, gaussianCascadeLog n x T ∂gaussianCascadeLaw n b v) =
        ((List.ofFn (fun i : Fin n => (b i, (v i : ℝ)))).foldr
          (fun av U => gaussianOperator av.1 av.2 U)
          (fun z => Real.log (Real.cosh z))) x := by
…

    Mentions: OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.gaussianCascadeLog, OAI.InvariantIsing.gaussianCascadeLaw, OAI.InvariantIsing.gaussianOperator