TensorCoordinateMinimum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual finite tensor coordinates at a penalized pressure minimum.

lemma OAI.InvariantIsing.tensorFrozenCGF_mean_bounds line 16

def OAI.InvariantIsing.tensorGaussianCoordinatePressure line 35

Source documentation

The coordinate pressure is the actual root/cascade pressure averaged over the rotation, with precisely one Gaussian amplitude replaced.

def tensorGaussianCoordinatePressure {N m : ℕ}
    (μ : Measure (SpecialOrthogonal N)) (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ) (amplitude : Fin N → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (r : Fin N → ℕ) (h : ℕ → ℝ) (j : Fin N) (w : ℝ) : ℝ :=
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal

lemma OAI.InvariantIsing.tensorGaussianCoordinatePressure_cost line 46

Source documentation

Applying the proved frozen-Gaussian mean estimate to the actual coordinate pressure requires only its already established second moments.

lemma tensorGaussianCoordinatePressure_cost {N m : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ) (amplitude : Fin N → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (r : Fin N → ℕ) (h : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (hb : CascadeExponents n b) (j : Fin N) (w : ℝ)
    (hF : ∀ a : ℝ, a = perturbationAmplitude N j * w ∨ a = 0 →
      MemLp (tensorDisorderPressure eig c I degree (Function.update amplitude j a) n) 2
        (μ.prod (tensorRootTreeLaw I degree n b
          (fun i => tensorPathProfile I degree n r h (i + 1)) (tensorPathProfile I degree n r h 0)))) :
    let M := tensorGaussianCoordinatePressure μ eig c I degree amplitude n b r h j
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.tensorGaussianCoordinatePressure

theorem OAI.InvariantIsing.tensorGaussianCoordinate_energy_at_minimum line 75

Source documentation

At a deterministic minimum of the actual Gaussian coordinate, its Gibbs energy concentrates around the derivative of the quadratic penalty.

theorem tensorGaussianCoordinate_energy_at_minimum {N m : ℕ} (hN : 0 < N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ) (amplitude : Fin N → ℝ)
    (n : ℕ) (b : ℕ → ℝ) (r : Fin N → ℕ) (h : ℕ → ℝ)
    (hh : Monotone h) (h0 : 0 ≤ h 0) (hb : CascadeExponents n b) (j : Fin N)
    (w s K B : ℝ) (hw : w ∈ Set.Icc (1 : ℝ) 2)
    (he : perturbationScale N ≤ 1 / 8) (hs : 0 < s) (hs' : s ≤ 1 / 4) (hK : 0 < K)
    (hF : ∀ v : ℝ, |v| ≤ 2 →
      MemLp (tensorDisorderPressure eig c I degree
        (Function.update amplitude j (perturbationAmplitude N j * v)) n) 2
        (μ.prod (tensorRootTreeLaw I degree n b
          (fun i => tensorPathProfile I degree n r h (i + 1)) (tensorPathProfile I degree n r h 0))))
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorDisorderPressure, OAI.InvariantIsing.tensorRootTreeLaw, OAI.InvariantIsing.tensorPathProfile