TensorZeroFieldPressure.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

With both the linear-field heights and the monomial amplitudes zero, the cascade leaves the original finite Ising pressure unchanged.

lemma OAI.InvariantIsing.vectorGaussianLaw_zero_ae line 16
lemma OAI.InvariantIsing.integral_vectorGaussianLaw_zero line 27
lemma OAI.InvariantIsing.logMean_vectorGaussianLaw_zero line 36
lemma OAI.InvariantIsing.rotatedCascadeValue_zero_variance line 43
lemma OAI.InvariantIsing.rotatedEnrichedPressure_zero_variance line 55
lemma OAI.InvariantIsing.varianceIncrement_zero_path line 62

theorem OAI.InvariantIsing.tensorPathPressure_zero_field line 66

Source documentation

The exact unperturbed pressure at zero field height, including the root.

theorem tensorPathPressure_zero_field {N m k : ℕ} (eig : Fin N → ℝ) (U : Rotation N)
    (c : Fin N → ℝ) (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ)
    (n : ℕ) (b : ℕ → ℝ) (hb : CascadeExponents n b) (r : Fin k → ℕ) :
    tensorEnrichedPressure eig U c I degree (fun _ => 0) n b
      (fun i => tensorPathProfile I degree n r (fun _ => 0) (i + 1))
      (tensorPathProfile I degree n r (fun _ => 0) 0) = rotatedPressure eig U c := by
…

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

theorem OAI.InvariantIsing.tensorNamespacedMeanPressure_zero_field_cost line 78

Source documentation

At zero random-field height the centered actual pressure differs from the ordinary Haar-mean pressure only by the established perturbation cost.

theorem tensorNamespacedMeanPressure_zero_field_cost
    (hhaar : HaarConcentrationInput) (hgauss : GaussianLipschitzVarianceInput)
    {N m : ℕ} (hN : 3 ≤ N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (hμ : μ.IsMulLeftInvariant)
    (eig c : Fin N → ℝ) (I : Fin m → Finset (Fin N))
    (u : Fin N → ℝ) (hu : ∀ j, |u j| ≤ 2) (v : Fin m → ℝ) (hv : ∀ j, |v j| ≤ 2)
    (t : ℝ) (n : ℕ) (b : ℕ → ℝ) (hb : CascadeExponents n b) :
    |tensorNamespacedMeanPressure μ (diagonalPerturbedEigenvalues eig I v t) c I
        (fun j => enumeratedSpectralDegree m j) (tensorPerturbationAmplitude N u)
        n b (fun j => enumeratedTreeDegree m j) (fun _ => 0) -
      ∫ U : SpecialOrthogonal N, rotatedPressure (fun i => t * eig i) (specialRotation U) c ∂μ| ≤
      2 * m * perturbationScale N + 8 * perturbationScale N ^ 2 := by
…

Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorNamespacedMeanPressure, OAI.InvariantIsing.diagonalPerturbedEigenvalues, OAI.InvariantIsing.enumeratedSpectralDegree, OAI.InvariantIsing.tensorPerturbationAmplitude, OAI.InvariantIsing.enumeratedTreeDegree, OAI.InvariantIsing.specialRotation

theorem OAI.InvariantIsing.tensorContactPressure_zero_field_cost line 105
theorem OAI.InvariantIsing.tensorContactPressure_one_zero_field_cost line 121