FullPerturbationCost.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform vanishing cost of both terms of the manuscript perturbation.

lemma OAI.InvariantIsing.rotatedEnergy_mul line 15
lemma OAI.InvariantIsing.abs_tensorPathPressure_sub_base_le line 20

theorem OAI.InvariantIsing.fullPerturbationPressure_cost line 60

Source documentation

The actual diagonal and Gaussian perturbations together cost at most 2 m e_N + 8 e_N², uniformly in the other deterministic parameters.

theorem fullPerturbationPressure_cost {N m : ℕ} (hN : 0 < N)
    (eig c : Fin N → ℝ) (U : Rotation N) (I : Fin m → Finset (Fin N))
    (degree : Fin N → Fin m → ℕ) (u : Fin N → ℝ) (hu : ∀ j, |u j| ≤ 2)
    (z : Fin m → ℝ) (hz : ∀ a, |z a| ≤ 2) (t : ℝ)
    (n : ℕ) (r : Fin N → ℕ) (b : ℕ → ℝ) (hb : CascadeExponents n b)
    (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0) :
    let v := tensorPathProfile I degree n r h
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.tensorPathProfile

lemma OAI.InvariantIsing.fullPerturbationCost_tendsto line 86