OAI/Probability/InvariantIsing/Arrays/TensorMinimumPenalty.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual minimizing objective has a vanishing penalty whenever its pressure has a uniform vanishing perturbation cost. Its negative minimum is the scalar pressure envelope used in the cavity telescoping argument.

  1. def OAI.InvariantIsing.tensorMinimumPenalty line 15
  2. lemma OAI.InvariantIsing.tensorMinimumPenalty_nonneg line 18
  3. lemma OAI.InvariantIsing.tensorMinimumPenalty_center line 23
  4. lemma OAI.InvariantIsing.tensorPerturbationObjective_eq line 27
  5. theorem OAI.InvariantIsing.tensor_minimum_envelope_cost line 38

    Source documentation

    A genuine minimum lies within the same uniform cost of the base pressure, and its quadratic penalty is at most twice that cost.

    theorem tensor_minimum_envelope_cost {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')
    (P δ : ℝ)
    (hcost : ∀ u' v', (∀ j, u' j ∈ Set.Icc (1 : ℝ) 2) →
      (∀ a, v' a ∈ Set.Icc (1 : ℝ) 2) →
…

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