PriorMinimumEnvelope.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Minimum envelopes for the actual fixed-prior model.

lemma OAI.InvariantIsing.priorPerturbationObjective_eq line 12

theorem OAI.InvariantIsing.prior_minimum_envelope_cost line 24

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 prior_minimum_envelope_cost {N m n : ℕ}
    (μ : Measure (SpecialOrthogonal N)) (ν : Measure (Spin N × LabeledLeaf n))
    (eig c : Fin N → ℝ)
    (I : Fin m → Finset (Fin N)) (t : ℝ) (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) →
      priorPerturbationObjective μ ν eig c I t h u v ≤
        priorPerturbationObjective μ ν eig c I t h u' v')
    (P δ : ℝ)
    (hcost : ∀ u' v', (∀ j, u' j ∈ Set.Icc (1 : ℝ) 2) →
…

Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.priorPerturbationObjective