FieldFiniteNeighborhood.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Every strictly positive finite covariance list admits the joint height derivative construction on a neighborhood of its parameter vector.

lemma OAI.InvariantIsing.fieldFinite_variance_neighborhood line 14
lemma OAI.InvariantIsing.fieldFinite_coefficient_bound line 37
lemma OAI.InvariantIsing.fieldFinite_slope_bound line 52
lemma OAI.InvariantIsing.fieldFinite_curvature_bound line 58
theorem OAI.InvariantIsing.fieldFiniteValue_local_family line 72
Source documentation
Joint gradient and symmetric Hessian data for the actual finite Gaussian recursion, constructed on a neighborhood of every strict covariance vector.
```
theorem fieldFiniteValue_local_family {n : ℕ} (L : List (FieldFiniteStep n))
    (h : Fin n → ℝ) (hpos : ∀ av ∈ L, 0 < fieldFiniteVariance av.base av.slope h) :
    ∃ (I : Set (Fin n → ℝ)) (_ : IsOpen I), h ∈ I ∧
      ∃ F : FieldFiniteFamily n I, F.U = fieldFiniteValue L := by
…
```
Mentions: OAI.InvariantIsing.FieldFiniteStep, OAI.InvariantIsing.fieldFiniteVariance, OAI.InvariantIsing.FieldFiniteFamily, OAI.InvariantIsing.fieldFiniteValue