GaussianMinorants.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Gaussian minorants with explicit interpolation coefficients

The atomic construction of the sharp Gaussian minorants gives the two order-twenty interpolation blocks and an absolutely summable correction. This formulation records the finite coefficients separately for the two Hermite basis functions, as in the atomic certificate of OpenAI.

def OAI.AtomicTriangular.Construction.correctedFinite line 21
Source documentation
The finite interpolation coefficients with the finite correction added.
Also declared: ComparatorChallenges/TriangularGaussian.lean:220 (same declaration text).
```
def correctedFinite (side : Fin 2) (z : ℝ) (δ : Fin 20 → ℝ) (j : Fin 22) : ℝ :=
…
```
def OAI.AtomicTriangular.AtomicConstruction line 40
Source documentation
The two atomic interpolation blocks and their summable correction reconstruct the minorant with the specified Gaussian normalization.
Distinct definitions of this name: ComparatorChallenges/TriangularGaussian.lean:236 (same statement text; different proof or body). Qualify references as OAI.AtomicTriangular.AtomicConstruction@path.
```
def AtomicConstruction (α : ℝ) (f : Plane → ℝ) : Prop :=
…
```
Mentions: OAI.AtomicTriangular.Plane
lemma OAI.AtomicTriangular.Construction.HasAtomicConstruction.atomicConstruction line 58
theorem OAI.AtomicTriangular.sharp_gaussian_minorants_with_construction line 73
Source documentation
Sharp radial Gaussian minorants have nonnegative Fourier transform, exact lattice contacts, and the atomic construction when the parameter is at least one.
Distinct definitions of this name: ComparatorChallenges/TriangularGaussian.lean:263 (same statement text; different proof or body). Qualify references as OAI.AtomicTriangular.sharp_gaussian_minorants_with_construction@path.
```
theorem sharp_gaussian_minorants_with_construction (α : ℝ) (hα : 0 < α) :
    ∃ f : SchwartzMap Plane ℝ,
      Radial f ∧ (∀ x, f x ≤ gaussian α x) ∧
      (∀ w, (realFourier f w).im = 0 ∧ 0 ≤ (realFourier f w).re) ∧
      (∀ a ∈ A, a ≠ 0 → f a = gaussian α a) ∧
      (∀ w ∈ dualA, w ≠ 0 → realFourier f w = 0) ∧
      (1 ≤ α → AtomicConstruction α f) := by
…
```
Mentions: OAI.AtomicTriangular.Plane, OAI.AtomicTriangular.Radial, OAI.AtomicTriangular.gaussian, OAI.AtomicTriangular.realFourier, OAI.AtomicTriangular.A, OAI.AtomicTriangular.dualA