MagneticFieldMinimum.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The finite prescribed-magnetization functional has an attained bias minimum at every interior magnetization. No optimizer or concavity premise is used.

def OAI.InvariantIsing.magneticBiasObjective line 16
Source documentation
The finite canonical field value with the magnetization constraint.
Also declared: ComparatorChallenges/InvariantIsing.lean:149 (same declaration text).
```
def magneticBiasObjective (h : FieldStep) (s b : ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
def OAI.InvariantIsing.constrainedFieldValue line 20
Source documentation
The prescribed-magnetization field functional from (mag:constrained-functional).
Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:151 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.constrainedFieldValue@path.
```
def constrainedFieldValue (h : FieldStep) (s : ℝ) : ℝ :=
…
```
Mentions: OAI.InvariantIsing.FieldStep
lemma OAI.InvariantIsing.magneticBiasObjective_lower line 23
lemma OAI.InvariantIsing.magneticBiasObjective_bddBelow line 32
lemma OAI.InvariantIsing.continuous_magneticBiasObjective line 39
lemma OAI.InvariantIsing.hasDerivAt_magneticBiasObjective line 43
lemma OAI.InvariantIsing.exists_magneticBias_minimum line 51
Source documentation
Linear coercivity gives a genuine global optimizer, including field profiles with tied heights or zero increments.
```
lemma exists_magneticBias_minimum (h : FieldStep) {s : ℝ} (hs : |s| < 1) :
    ∃ b : ℝ, ∀ c : ℝ, magneticBiasObjective h s b ≤ magneticBiasObjective h s c := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.magneticBiasObjective
lemma OAI.InvariantIsing.constrainedFieldValue_eq_at_minimum line 85
lemma OAI.InvariantIsing.constrainedFieldValue_attained line 93
lemma OAI.InvariantIsing.magneticBiasMean_eq_of_minimum line 101
Source documentation
At any minimizing bias the actual physical mean spin equals the prescribed magnetization.
```
lemma magneticBiasMean_eq_of_minimum (h : FieldStep) {s b : ℝ}
    (hmin : ∀ c : ℝ, magneticBiasObjective h s b ≤ magneticBiasObjective h s c) :
    fieldBiasMean h b = s := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.magneticBiasObjective, OAI.InvariantIsing.fieldBiasMean
lemma OAI.InvariantIsing.constrainedFieldValue_coe_iInf line 109
Source documentation
The real minimum agrees exactly with the extended-real infimum.
```
lemma constrainedFieldValue_coe_iInf (h : FieldStep) {s : ℝ} (hs : |s| < 1) :
    (constrainedFieldValue h s : EReal) =
      ⨅ b : ℝ, ((fieldValue h b - b * s : ℝ) : EReal) := by
…
```
Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.fieldValue

lemma OAI.InvariantIsing.magneticBias_minimum_bound line 122

Source documentation

Interior minimizing biases are bounded uniformly on bounded-height families of fields.

lemma magneticBias_minimum_bound (h : FieldStep) {s b C : ℝ} (hs : |s| < 1)
    (hC : h.height (Fin.last h.depth) ≤ C)
    (hmin : ∀ c : ℝ, magneticBiasObjective h s b ≤ magneticBiasObjective h s c) :
    |b| ≤ (Real.log 2 + C / 2) / (1 - |s|) := by
…

Mentions: OAI.InvariantIsing.FieldStep, OAI.InvariantIsing.magneticBiasObjective