NSpinCascadeFluctuation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional cascade fluctuations for the actual Ising terminal.

theorem OAI.InvariantIsing.rotatedCascadeLog_centered_square line 16

Source documentation

The conditional cascade fluctuation is bounded uniformly in the Ising terminal, rotation, external field, Gaussian root and number of spins.

theorem rotatedCascadeLog_centered_square {N : ℕ} (hN : 0 < N)
    (n : ℕ) (b : ℕ → ℝ) (v : ℕ → ℝ≥0) (hb : IsingPerceptron.CascadeExponents n b)
    (eig : Fin N → ℝ) (U : Rotation N) (c z : Fin N → ℝ) :
    Integrable (fun T => (rotatedCascadeLog n eig U c z T -
      rotatedCascadeValue n b v eig U c z) ^ 2) (rotatedCascadeLaw N n b v) ∧
    (∫ T, (rotatedCascadeLog n eig U c z T - rotatedCascadeValue n b v eig U c z) ^ 2
      ∂rotatedCascadeLaw N n b v) ≤
      4 * ∫ T, (Real.log (IsingPerceptron.rawTreeTotal n T).toReal) ^ 2
        ∂(IsingPerceptron.rawCascadeLaw n b : Measure (IsingPerceptron.RawTree n)) := by
…

Mentions: OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.rotatedCascadeLog, OAI.InvariantIsing.rotatedCascadeValue, OAI.InvariantIsing.rotatedCascadeLaw, OAI.IsingPerceptron.rawTreeTotal, OAI.IsingPerceptron.rawCascadeLaw, OAI.IsingPerceptron.RawTree