OAI/Probability/InvariantIsing/Arrays/PerturbationWeights.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite perturbation sums for the manuscript's geometric weights.

  1. lemma OAI.InvariantIsing.perturbationWeight_linear_le line 14
  2. lemma OAI.InvariantIsing.perturbationWeight_degree_sum_le line 28
  3. def OAI.InvariantIsing.tensorPerturbationAmplitude line 46
  4. lemma OAI.InvariantIsing.tensorPerturbationAmplitude_update line 49
  5. lemma OAI.InvariantIsing.tensorPerturbationAmplitude_sq_le line 59
  6. lemma OAI.InvariantIsing.tensorPerturbationAmplitude_square_sum_le line 69
  7. lemma OAI.InvariantIsing.perturbationScale_le_one line 85
  8. lemma OAI.InvariantIsing.perturbationScale_sq_le_one line 90
  9. theorem OAI.InvariantIsing.tensorPerturbationAmplitude_degree_sum_le line 97

    Source documentation

    The fixed linear bound on the enumerated monomial degrees gives a dimension-independent normalized rotation modulus. Only the finite sum through dimension N is used.

    theorem tensorPerturbationAmplitude_degree_sum_le {N m : ℕ}
    (u : Fin N → ℝ) (hu : ∀ j, |u j| ≤ 2) (degree : Fin N → Fin m → ℕ)
    (D : ℝ) (hD : 0 ≤ D)
    (hdegree : ∀ j, (∑ a, (degree j a : ℝ)) ≤ D * ((j : ℝ) + 1)) :
    (∑ j : Fin N, tensorPerturbationAmplitude N u j ^ 2 * ∑ a, (degree j a : ℝ)) ≤
      4 * N * perturbationScale N ^ 2 * D := by
…

    Mentions: OAI.InvariantIsing.tensorPerturbationAmplitude