OAI/Probability/InvariantIsing/Arrays/TensorObjectiveContinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.tensorPathPressure_haar_mean line 16
2. lemma OAI.InvariantIsing.rotatedEnergy_diagonal_difference_le line 52
3. lemma OAI.InvariantIsing.tensorPerturbationPressureMean_modulus line 71
4. lemma OAI.InvariantIsing.continuous_tensorPerturbationPressureMean line 115
5. lemma OAI.InvariantIsing.continuous_tensorPerturbationObjective line 140
6. lemma OAI.InvariantIsing.finiteBox_minimum line 152
7. theorem OAI.InvariantIsing.tensorPerturbationObjective_exists_minimum line 174

   Source documentation

   The minimizers required by the GG/contact estimates exist for the actual finite objective on the manuscript's compact perturbation box.

   theorem tensorPerturbationObjective_exists_minimum (hhaar : HaarConcentrationInput)
       (hgauss : GaussianLipschitzVarianceInput) {N m : ℕ} (hN : 3 ≤ N)
       (μ : Measure (SpecialOrthogonal N)) [IsProbabilityMeasure μ] (hμ : μ.IsMulLeftInvariant)
       (eig c : Fin N → ℝ) (I : Fin m → Finset (Fin N)) (t : ℝ)
       (n : ℕ) (b : ℕ → ℝ) (hb : CascadeExponents n b)
       (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0) :
       ∃ u : Fin N → ℝ, ∃ v : Fin m → ℝ,
         (∀ j, u j ∈ Set.Icc (1 : ℝ) 2) ∧ (∀ a, v a ∈ Set.Icc (1 : ℝ) 2) ∧
         ∀ 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' := by
   …

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