TensorMinimumPressure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual zero-field perturbation minima approximate the unperturbed Haar pressure, with a uniform cost independent of the auxiliary cascade depth.

theorem OAI.InvariantIsing.tensor_zero_field_minimum_cost line 15

theorem OAI.InvariantIsing.tensor_zero_field_minimum_tendsto line 42

Source documentation

Both errors vanish along any diverging sequence of physical dimensions. No fixed-depth assumption is required.

theorem tensor_zero_field_minimum_tendsto
    (hhaar : HaarConcentrationInput) (hgauss : GaussianLipschitzVarianceInput)
    (N : ℕ → ℕ) (hN : ∀ r, 3≤N r) (hNlim : Tendsto N atTop atTop) (m : ℕ)
    (μ : (r : ℕ) → Measure (SpecialOrthogonal (N r))) [∀ r, IsProbabilityMeasure (μ r)]
    (hμ : ∀ r, (μ r).IsMulLeftInvariant)
    (eig c : (r : ℕ) → Fin (N r) → ℝ) (I : (r : ℕ) → Fin m → Finset (Fin (N r)))
    (t : ℕ → ℝ) (n : ℕ → ℕ) (b : ℕ → ℕ → ℝ) (hb : ∀ r, CascadeExponents (n r) (b r))
    (u : (r : ℕ) → Fin (N r) → ℝ) (v : ℕ → Fin m → ℝ)
    (hu : ∀ r j, u r j ∈ Set.Icc (1 : ℝ) 2) (hv : ∀ r a, v r a ∈ Set.Icc (1 : ℝ) 2)
    (hmin : ∀ r u' v', (∀ j, u' j ∈ Set.Icc (1 : ℝ) 2) →
      (∀ a, v' a ∈ Set.Icc (1 : ℝ) 2) →
      tensorPerturbationObjective (μ r) (eig r) (c r) (I r) (t r) (n r) (b r) (fun _ => 0) (u r) (v r) ≤
…

Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorPerturbationObjective