HeatGramError.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Relative error of actual heat Gram matrices

After normalizing the coordinate columns, local Gram error and missing heat mass control the operator error. The estimates use the actual carré du champ and the same kernel as the heat construction.

theorem OAI.RegularPointCoordinates.weightedGram_sub_mass_id_norm_le line 26

Source documentation

Weighted first-order splitting errors bound the Gram operator relative to the mass of the weight. No normalization of the weight is assumed.

theorem weightedGram_sub_mass_id_norm_le {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) {w : X → ℝ}
    (hw : AEStronglyMeasurable w μ) {C : ℝ≥0}
    (hb : ∀ᵐ x ∂μ, ‖w x‖ ≤ (C : ℝ)) (hiw : Integrable w μ)
    (hpos : ∀ᵐ x ∂μ, 0 ≤ w x) {epsilon : ℝ} (heps : 0 ≤ epsilon)
    (herr : ∀ i j : Fin n, ∫ x, w x *
      |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ ≤ epsilon) :
    ‖sobolevGram μ hQ (sobolevColumnMap μ hQ u) hw hb -
      (∫ x, w x ∂μ) • ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤ (n : ℝ) ^ 2 * epsilon := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.sobolevGram, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.cutoffHeatGram_sub_id_norm_le line 69

Source documentation

In normalized columns the heat Gram error is bounded by the weighted Gram defect, the lost heat mass, and the exact scalar regularizer.

theorem cutoffHeatGram_sub_id_norm_le {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (hχpos : ∀ y, 0 ≤ χ y)
    {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) {epsilon : ℝ} (heps : 0 ≤ epsilon)
    (herr : ∀ i j : Fin n, ∫ y, (χ y * p t x y) *
      |localGamma μ hQ (u i) (u j) y - (if i = j then 1 else 0)| ∂μ ≤ epsilon) :
    ‖cutoffHeatGram μ hQ hp hχ hsχ (sobolevColumnMap μ hQ u) ht x lambda -
      ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤
      (n : ℝ) ^ 2 * epsilon + |(∫ y, χ y * p t x y ∂μ) - 1| + |lambda * t| := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.cutoffHeatGram_conjugate line 109

Source documentation

The scalar regularizer transforms into A* A. This identity keeps the conjugated original heat matrix distinct from a freshly regularized Gram matrix of the transformed columns.

theorem cutoffHeatGram_conjugate {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E]
    (U : E →L[ℝ] SobolevSpace μ hQ) (A : E →L[ℝ] E)
    {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) :
    A.adjoint.comp ((cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda).comp A) =
      sobolevGram μ hQ (U.comp A)
        ((hχ.mul (hp.continuous_right t ht x)).aestronglyMeasurable)
        (Filter.Eventually.of_forall (cutoffHeatWeight_le μ hQ hp hχ hsχ ht x)) +
      (lambda * t) • A.adjoint.comp A := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.cutoffHeatGram, OAI.RegularPointCoordinates.sobolevGram, OAI.RegularPointCoordinates.cutoffHeatWeight_le

theorem OAI.RegularPointCoordinates.sobolevColumnMap_basis_values line 126
Source documentation
Reconstruct a finite coordinate column from its values on the Euclidean basis.
```
theorem sobolevColumnMap_basis_values {n : ℕ}
    (U : Euclidean n →L[ℝ] SobolevSpace μ hQ) :
    sobolevColumnMap μ hQ (fun i => U (EuclideanSpace.single i 1)) = U := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.cutoffHeatGram_conjugated_sub_id_norm_le line 139

Source documentation

Relative comparison in an arbitrary normalized frame. The cost of the regularizer is the squared norm of that frame, as required at small scales.

theorem cutoffHeatGram_conjugated_sub_id_norm_le {n : ℕ}
    (U : Euclidean n →L[ℝ] SobolevSpace μ hQ) (A : Euclidean n →L[ℝ] Euclidean n)
    (hχpos : ∀ y, 0 ≤ χ y) {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ)
    {epsilon : ℝ} (heps : 0 ≤ epsilon)
    (herr : ∀ i j : Fin n, ∫ y, (χ y * p t x y) *
      |localGamma μ hQ (U (A (EuclideanSpace.single i 1)))
        (U (A (EuclideanSpace.single j 1))) y - (if i = j then 1 else 0)| ∂μ ≤ epsilon) :
    ‖A.adjoint.comp ((cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda).comp A) -
      ContinuousLinearMap.id ℝ (Euclidean n)‖ ≤
      (n : ℝ) ^ 2 * epsilon + |(∫ y, χ y * p t x y ∂μ) - 1| +
        |lambda * t| * ‖A‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.cutoffHeatGram