UniformPolarizedError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform operator control from finitely many scalar cutoff errors

theorem OAI.RegularPointCoordinates.polarizedDerivative_uniformly_small line 19

Source documentation

Finitely many coordinate tests turn uniform scalar decay into uniform operator decay; the scalar threshold may initially depend on the direction.

theorem polarizedDerivative_uniformly_small {X : Type*} {n : ℕ}
    (d : ℝ → X → Euclidean n → ℝ) (P : Set X)
    (hd : ∀ v, ∀ η : ℝ, 0 < η → ∃ δ : ℝ, 0 < δ ∧
      ∀ t, 0 < t → t < δ → ∀ x ∈ P, |d t x v| < η)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ t, 0 < t → t < δ → ∀ x ∈ P,
      ‖polarizedDerivative (d t x)‖ < ε := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative

def OAI.RegularPointCoordinates.harmonicHeatError line 64
Source documentation
The operator cutoff error is built from the actual scalar product-rule sources. It is not an additional analytic input.
```
def harmonicHeatError {n : ℕ} {U : Euclidean n →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X (Euclidean n)} {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
    {ρ C : ℝ} (χ : GoodLaplacianCutoff μ hQ p ρ C) (t : ℝ) (x : X) :
    Euclidean n →L[ℝ] Euclidean n :=
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff

theorem OAI.RegularPointCoordinates.harmonicHeatError_uniformly_small line 75

Source documentation

Local Euclidean volume bounds make the canonical error uniformly small in operator norm throughout the inner pole ball.

theorem harmonicHeatError_uniformly_small (hg : HasCoordinateHeatBounds μ k)
    {n : ℕ} {U : Euclidean n →L[ℝ] SobolevSpace μ hQ}
    {M : PositiveBilinearMeasure X (Euclidean n)} {κ : ℝ} {p : X} {r : ℝ} {L : ℝ≥0}
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p r L v)
    {ρ C D V : ℝ} (χ : GoodLaplacianCutoff μ hQ p ρ C)
    (hρ : 0 < ρ) (hD : 0 < D) (hV : 0 < V)
    (hvol : ∀ y, ρ ≤ dist p y → dist p y ≤ 2 * ρ →
      ∀ s, 0 < s → s ≤ D → V * s ^ n ≤ μ.real (Metric.ball y s))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ t, 0 < t → t < δ → ∀ x ∈ Metric.ball p (ρ / 2),
      ‖harmonicHeatError μ hQ (k := k) G χ t x‖ < ε := by
…

Mentions: OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.harmonicHeatError