TensorPerturbationCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the actual Gaussian monomial perturbation has vanishing pressure cost.

lemma OAI.InvariantIsing.tensorLeafCoefficients_mixed_cross line 17
lemma OAI.InvariantIsing.tensorLeafCoefficients_zero_cross line 47
lemma OAI.InvariantIsing.tensorPath_monomial_increment_cross_le line 71
Source documentation
The linear enrichment contributes no covariance to the increment obtained by removing all monomial amplitudes. The remaining covariance is bounded by the sum of their squared amplitudes, independently of depth.
```
lemma tensorPath_monomial_increment_cross_le {N m k : ℕ} (U : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
    (a : Fin k → ℝ) (n : ℕ) (r : Fin k → ℕ) (h : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (x y : Spin N × LabeledLeaf n) :
    let A := tensorLeafCoefficients U I degree a n (fun i => tensorPathProfile I degree n r h i)
…
```
Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorLeafCoefficients, OAI.InvariantIsing.tensorPathProfile
theorem OAI.InvariantIsing.tensorPathLogMean_monomial_cost line 106
theorem OAI.InvariantIsing.abs_tensorPathPressure_sub_zero_amplitude_le line 125

theorem OAI.InvariantIsing.tensorPerturbationPressure_cost line 159

Source documentation

The paper's finite monomial perturbation changes the enriched mean pressure by at most 8 e_N², uniformly in the rotation and tree depth.

theorem tensorPerturbationPressure_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)
    (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