TensorPerturbationObjective.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Global minima of the actual finite perturbation objective imply both coordinate minimum conditions used by the GG estimates.

def OAI.InvariantIsing.tensorPerturbationObjective line 15
lemma OAI.InvariantIsing.penalty_update line 22
Also declared: OAI/Probability/InvariantIsing/Fields/PriorMinimumCoordinates.lean:27 (same declaration text), OAI/Probability/InvariantIsing/Fields/SpinPriorMinimumCoordinates.lean:22 (same declaration text).
lemma OAI.InvariantIsing.update_mem_Icc line 36
Also declared: OAI/Probability/InvariantIsing/Fields/PriorMinimumCoordinates.lean:41 (same declaration text), OAI/Probability/InvariantIsing/Fields/SpinPriorMinimumCoordinates.lean:36 (same declaration text).

theorem OAI.InvariantIsing.tensorPerturbation_minimum_coordinates line 46

Source documentation

This is a direct restriction of the genuine joint finite-model minimum.

theorem tensorPerturbation_minimum_coordinates {N m : ℕ}
    (μ : Measure (SpecialOrthogonal N)) (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (t : ℝ) (n : ℕ) (b h : ℕ → ℝ)
    (u : Fin N → ℝ) (v : Fin m → ℝ)
    (hu : ∀ j, u j ∈ Set.Icc (1 : ℝ) 2) (hv : ∀ a, v a ∈ Set.Icc (1 : ℝ) 2)
    (hmin : ∀ u' v', (∀ j, u' j ∈ Set.Icc (1 : ℝ) 2) → (∀ a, v' a ∈ Set.Icc (1 : ℝ) 2) →
      tensorPerturbationObjective μ eig c I t n b h u v ≤ tensorPerturbationObjective μ eig c I t n b h u' v') :
    let M := tensorPerturbationPressureMean μ eig c I (n := n) (b := b) (h := h)
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorPerturbationObjective, OAI.InvariantIsing.tensorPerturbationPressureMean