TensorContactCap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The field cap in the fixed-partition contact problem is inactive on negative sublevels. All estimates concern the actual perturbed pressure.

lemma OAI.InvariantIsing.tensorContactPressure_field_le line 17

theorem OAI.InvariantIsing.tensorContactObjective_cap_bound line 76

Source documentation

A coercive lower bound in the total nonnegative field increment.

theorem tensorContactObjective_cap_bound
    (hhaar : HaarConcentrationInput) (hgauss : GaussianLipschitzVarianceInput)
    {N m n : ℕ} (hN : 3 ≤ N)
    (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (hμ : μ.IsMulLeftInvariant)
    (eig : Fin N → ℝ) (I : Fin m → Finset (Fin N)) (K : ℝ)
    (heig : ∀ i, |eig i| ≤ K)
    (cut : Fin (n + 2) → ℝ) (hc : StrictMono cut)
    (hfirst : cut 0 = 0) (hlast : cut (Fin.last (n + 1)) = 1)
    (trial : OverlapPath) (values : Fin (n + 1) → ℝ)
    (hvalues : ∀ i s, s ∈ Ioo (cut i.castSucc) (cut i.succ) → trial s = values i)
    (d : ℝ) (hd : 0 ≤ d) (htrial : ∀ᵐ s ∂pathMeasure, trial s ≤ 1 - d)
    (S : ℝ) (V : ℝ → ℝ) (p : TensorContactParameter N m n)
…

Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.TensorContactParameter

theorem OAI.InvariantIsing.exists_tensorContactObjective_cap line 120

Source documentation

One fixed cap works for every dimension and every allowed perturbation parameter. Thus a negative contact sublevel cannot touch its field face.

theorem exists_tensorContactObjective_cap
    (hhaar : HaarConcentrationInput) (hgauss : GaussianLipschitzVarianceInput)
    (m n : ℕ) (cut : Fin (n + 2) → ℝ) (hc : StrictMono cut)
    (hfirst : cut 0 = 0) (hlast : cut (Fin.last (n + 1)) = 1)
    (trial : OverlapPath) (values : Fin (n + 1) → ℝ)
    (hvalues : ∀ i s, s ∈ Ioo (cut i.castSucc) (cut i.succ) → trial s = values i)
    (d : ℝ) (hd : 0 < d) (htrial : ∀ᵐ s ∂pathMeasure, trial s ≤ 1 - d)
    (K S L : ℝ) :
    ∃ H : ℝ, 0 < H ∧ ∀ (N : ℕ) (_hN : 3 ≤ N)
      (μ : Measure (SpecialOrthogonal N)) (_hμprob : IsProbabilityMeasure μ)
      (_hμ : μ.IsMulLeftInvariant) (eig : Fin N → ℝ) (I : Fin m → Finset (Fin N))
      (_heig : ∀ i, |eig i| ≤ K) (V : ℝ → ℝ)
…

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