OAI/Probability/InvariantIsing/Pressure/PressureCoordinateMinimum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.pressureCoordinate_minimum_rescale line 13
2. lemma OAI.InvariantIsing.gaussianCoordinate_minimum_penalty line 42

   Source documentation

   Comparing a Gaussian-coordinate minimum with its centered choice puts it in the interior, using the Gaussian variance cap of the frozen field.

   lemma gaussianCoordinate_minimum_penalty {N : ℕ} (hN : 0 < N) (j : Fin N)
       (M : ℝ → ℝ) (u : ℝ) (hu : |u| ≤ 2)
       (hcost : 0 ≤ M (3 / 2) - M 0 ∧ M u - M 0 ≤ (perturbationAmplitude N j * u) ^ 2 / (2 * N))
       (hmin : -M u + perturbationWeight j * (u - 3 / 2) ^ 2 ≤
         -M (3 / 2) + perturbationWeight j * (3 / 2 - 3 / 2) ^ 2) :
       (u - 3 / 2) ^ 2 ≤ 2 * perturbationScale N ^ 2 * perturbationWeight j := by
   …

3. lemma OAI.InvariantIsing.gaussianCoordinate_minimum_interior line 65
4. lemma OAI.InvariantIsing.diagonalCoordinate_minimum_penalty line 76
5. lemma OAI.InvariantIsing.diagonalCoordinate_minimum_interior line 82