ScaledProjectionOuter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform outer control after the physical projection rescaling

theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.scaled_projected_residual_outer line 19

Source documentation

The physical projection and forcing both have size r². Dividing both by that factor gives the same uniform transport and coefficient bounds; the radial error retains its natural length scale.

theorem LocalHarmonicL2GradientInput.scaled_projected_residual_outer
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    {κ H V W B J E D : ℝ} (hκ : 0 ≤ κ) (hH : 0 ≤ H) (hV : 0 ≤ V)
    (hW : 0 ≤ W) (hB : 0 ≤ B) (hJ : 0 ≤ J) (hE : 0 ≤ E) (Cw : ℝ≥0) :
    ∃ G T : ℝ, 0 ≤ G ∧ 0 ≤ T ∧
      ∀ (p : X) (R a r : ℝ), 0 < R → 0 ≤ a → a ≤ (n : ℝ) + 1 → -κ ≤ K * R ^ 2 → 0 < r →
      ∀ (f w η e : SobolevSpace (hausdorff n X) hX.quadratic)
        (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
        (N : Euclidean n ≃L[ℝ] Euclidean n) (ell : Euclidean n) (k σ : ℝ), 0 ≤ σ →
      IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (4 * R)) f a →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsConstantLaplacianOn