HeatGramRebase.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Returning the heat comparison to the original coordinate frame

theorem OAI.RegularPointCoordinates.cutoffHeatGram_rebase line 24

Source documentation

Rebasing the columns preserves the unregularized normalized heat matrix; the original regularizer contributes its exact conjugate.

theorem cutoffHeatGram_rebase (U : E →L[ℝ] SobolevSpace μ hQ)
    (T A : E ≃L[ℝ] E) {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ) :
    (A : E →L[ℝ] E).adjoint.comp
      ((cutoffHeatGram μ hQ hk hχ hsχ U ht x lambda).comp (A : E →L[ℝ] E)) =
    (A.trans T.symm : E →L[ℝ] E).adjoint.comp
      ((cutoffHeatGram μ hQ hk hχ hsχ (U.comp (T : E →L[ℝ] E)) ht x 0).comp
        (A.trans T.symm : E →L[ℝ] E)) +
      (lambda * t) • (A : E →L[ℝ] E).adjoint.comp (A : E →L[ℝ] E) := by
…

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

theorem OAI.RegularPointCoordinates.cutoffHeatGram_rebase_norm_le line 38

Source documentation

The scalar regularizer in the original frame costs the squared norm of the one working-scale normalization. This constant is independent of all subsequent finer scales.

theorem cutoffHeatGram_rebase_norm_le (U : E →L[ℝ] SobolevSpace μ hQ)
    (T A : E ≃L[ℝ] E) {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ)
    {b : ℝ} (hA : ‖(A.trans T.symm : E →L[ℝ] E)‖ ^ 2 ≤ b) :
    ‖(A : E →L[ℝ] E).adjoint.comp
        ((cutoffHeatGram μ hQ hk hχ hsχ U ht x lambda).comp (A : E →L[ℝ] E)) -
      ContinuousLinearMap.id ℝ E‖ ≤
    ‖(A.trans T.symm : E →L[ℝ] E).adjoint.comp
        ((cutoffHeatGram μ hQ hk hχ hsχ (U.comp (T : E →L[ℝ] E)) ht x 0).comp
          (A.trans T.symm : E →L[ℝ] E)) - ContinuousLinearMap.id ℝ E‖ +
      |lambda * t| * ‖(T : E →L[ℝ] E)‖ ^ 2 * b := by
…

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

theorem OAI.RegularPointCoordinates.exists_rebased_regularizer_threshold line 71

Source documentation

A fixed bound for the working frame permits a uniform fine-scale choice for the original scalar regularizer.

theorem exists_rebased_regularizer_threshold {B R lambda η : ℝ}
    (hB : 0 ≤ B) (hη : 0 < η) :
    ∃ N : ℕ, ∀ k, N ≤ k → ∀ r, 0 ≤ r → (2 : ℝ) ^ k * r ≤ R →
      ∀ T : E →L[ℝ] E, ‖T‖ ^ 2 ≤ B →
        |lambda * r ^ 2| * ‖T‖ ^ 2 * (2 : ℝ) ^ k < η := by
…