OAI/Probability/InvariantIsing/Fields/CascadeTilt.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.gaussianCascadeMarks line 15
2. def OAI.InvariantIsing.gaussianCascadeUpdate line 18
3. def OAI.InvariantIsing.gaussianCascadeBackward line 21
4. def OAI.InvariantIsing.gaussianCascadeMultiplier line 25
5. lemma OAI.InvariantIsing.measurable_gaussianCascadeUpdate line 30
6. lemma OAI.InvariantIsing.measurable_gaussianCascadeBackward line 33
7. lemma OAI.InvariantIsing.measurable_gaussianCascadeMultiplier line 38
8. lemma OAI.InvariantIsing.gaussianCascadeMultiplier_pos line 44
9. lemma OAI.InvariantIsing.gaussianCascadeMultiplier_moment line 49

   Source documentation

   Every edge multiplier is normalized under the exponent of its cascade level.

   lemma gaussianCascadeMultiplier_moment (n : ℕ) (b : ℕ → ℝ) (v : ℕ → ℝ≥0)
       (hb : IsingPerceptron.CascadeExponents n b) (i : ℕ) (x : ℝ) :
       (∫⁻ g, ENNReal.ofReal (gaussianCascadeMultiplier n b v i (x, g) ^ b i)
         ∂gaussianReal 0 (v i)) = 1 := by
   …

   Mentions: OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.gaussianCascadeMultiplier

10. def OAI.InvariantIsing.gaussianCascadeDisplacement line 61
11. theorem OAI.InvariantIsing.gaussianCascadeDisplacement_law line 67

    Source documentation

    The exact unmarked-law part of arr:rpc for Gaussian log cosh marks.

    theorem gaussianCascadeDisplacement_law (n : ℕ) (b : ℕ → ℝ) (v : ℕ → ℝ≥0)
        (hb : IsingPerceptron.CascadeExponents n b) (x : ℝ) :
        (gaussianCascadeLaw n b v).map (gaussianCascadeDisplacement n b v x) =
          IsingPerceptron.rawCascadeLaw n b := by
    …

    Mentions: OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.gaussianCascadeLaw, OAI.InvariantIsing.gaussianCascadeDisplacement, OAI.IsingPerceptron.rawCascadeLaw