DirectionalHeatError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Heat Gram error from directional L1 control

Quadratic-form estimates give operator estimates without a second coordinate polarization loss. The same normalizing frame is used in the heat matrix and in every directional error integral.

theorem OAI.RegularPointCoordinates.sobolevGram_sub_mass_quadratic line 26

Source documentation

The quadratic form of the mass-centered Gram is the weighted pointwise directional error.

theorem sobolevGram_sub_mass_quadratic (U : E →L[ℝ] SobolevSpace μ hQ)
    {w : X → ℝ} (hw : AEStronglyMeasurable w μ) {C : ℝ≥0}
    (hb : ∀ᵐ x ∂μ, ‖w x‖ ≤ (C : ℝ)) (hiw : Integrable w μ) (v : E) :
    ⟪v, (sobolevGram μ hQ U hw hb -
      (∫ x, w x ∂μ) • ContinuousLinearMap.id ℝ E) v⟫_ℝ =
      ∫ x, w x * (localGamma μ hQ (U v) (U v) x - ‖v‖ ^ 2) ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.weightedGram_sub_mass_norm_le_of_directional line 43

Source documentation

A bound in every constant direction controls the entire Gram error.

theorem weightedGram_sub_mass_norm_le_of_directional
    (U : E →L[ℝ] SobolevSpace μ hQ)
    {w : X → ℝ} (hw : AEStronglyMeasurable w μ) {C : ℝ≥0}
    (hb : ∀ᵐ x ∂μ, ‖w x‖ ≤ (C : ℝ)) (hiw : Integrable w μ)
    (hpos : ∀ᵐ x ∂μ, 0 ≤ w x) {ε : ℝ} (hε : 0 ≤ ε)
    (herr : ∀ v : E, (∫ x, w x * |localGamma μ hQ (U v) (U v) x - ‖v‖ ^ 2| ∂μ) ≤
      ε * ‖v‖ ^ 2) :
    ‖sobolevGram μ hQ U hw hb - (∫ x, w x ∂μ) • ContinuousLinearMap.id ℝ E‖ ≤ ε := by
…

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

theorem OAI.RegularPointCoordinates.cutoffHeatGram_conjugated_norm_le_of_directional line 67

Source documentation

Relative heat/mean error, including the actual conjugated scalar regularizer. There is no extra dimension factor.

theorem cutoffHeatGram_conjugated_norm_le_of_directional
    (U : E →L[ℝ] SobolevSpace μ hQ) (A : E →L[ℝ] E)
    (hχpos : ∀ y, 0 ≤ χ y) {t : ℝ} (ht : 0 < t) (x : X) (lambda : ℝ)
    {ε : ℝ} (hε : 0 ≤ ε)
    (herr : ∀ v : E, (∫ y, (χ y * p t x y) *
      |localGamma μ hQ (U (A v)) (U (A v)) y - ‖v‖ ^ 2| ∂μ) ≤ ε * ‖v‖ ^ 2) :
    ‖A.adjoint.comp ((cutoffHeatGram μ hQ hp hχ hsχ U ht x lambda).comp A) -
      ContinuousLinearMap.id ℝ E‖ ≤
      ε + |(∫ y, χ y * p t x y ∂μ) - 1| + |lambda * t| * ‖A‖ ^ 2 := by
…

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