GeometricProjectionOuter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform outer control for the actual projected Euler equation

theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.projected_residual_outer line 19

Source documentation

The local harmonic estimate controls the affine forcing from the inner residual. The radial transport estimate then controls its outer norm, with both constants preceding all centers and radii.

theorem LocalHarmonicL2GradientInput.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 : ℝ), 0 < R → 0 ≤ a → a ≤ (n : ℝ) + 1 → -κ ≤ K * R ^ 2 →
      ∀ (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