RegularizedGram.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Positive regularization of genuine Sobolev Gram operators

def OAI.RegularPointCoordinates.regularizedSobolevGram line 23
Source documentation
In the heat construction, w is the cutoff heat-kernel weight and a is the positive scalar regularization lambda * t.
```
def regularizedSobolevGram (a : ℝ) : E →L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.regularizedSobolevGram_energy line 26
theorem OAI.RegularPointCoordinates.regularizedSobolevGram_isPositive line 35
theorem OAI.RegularPointCoordinates.regularizedSobolevGram_coercive line 41
theorem OAI.RegularPointCoordinates.regularizedSobolevGram_injective line 51
def OAI.RegularPointCoordinates.regularizedSobolevGramEquiv line 64
Source documentation
The actual inverse exists in finite dimension; it need not be added as a hypothesis in the later heat-matrix estimates.
```
def regularizedSobolevGramEquiv [FiniteDimensional ℝ E]
    (hwpos : ∀ᵐ x ∂μ, 0 ≤ w x) {a : ℝ} (ha : 0 < a) : E ≃L[ℝ] E :=
…
```
theorem OAI.RegularPointCoordinates.regularizedSobolevGramEquiv_apply line 69

theorem OAI.RegularPointCoordinates.regularizedSobolevGramEquiv_symm_norm_le line 75

Source documentation

The positive regularization supplies a quantitative inverse bound.

theorem regularizedSobolevGramEquiv_symm_norm_le [FiniteDimensional ℝ E]
    (hwpos : ∀ᵐ x ∂μ, 0 ≤ w x) {a : ℝ} (ha : 0 < a) (v : E) :
    ‖(regularizedSobolevGramEquiv μ hQ U hw hb hwpos ha).symm v‖ ≤ a⁻¹ * ‖v‖ := by
…

Mentions: OAI.RegularPointCoordinates.regularizedSobolevGramEquiv