NoProjectedEulerSequence.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Excluding the actual normalized orthogonal projection sequence

theorem OAI.RegularPointCoordinates.no_projected_euler_sequence line 21
Source documentation
The unnormalized projection residual cannot dominate its source error along a geometric compactness sequence. All equations here are actual Sobolev equations, and orthogonality follows from the actual projection. The fixed outer constant changes the limit norm to M⁻², which stays nonzero.
```
theorem no_projected_euler_sequence {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hcompact : LocalPoissonHarmonicCompactnessInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
    {S ρ M C : ℝ} (hS : 0 < S) (hρ : 0 < ρ) (hρS : ρ < S) (hM : 0 < M)
    (q : RadialCompactnessSequence hX S)
    (v w e : ℕ → SobolevSpace (hausdorff n X) hX.quadratic)
    (b : ℕ → Euclidean n) (k B : ℕ → ℝ)
    (hf : ∀ i, ∀ᵐ x ∂(hausdorff n X).restrict (ball (q.center i) (S * q.radius i)),
      localGamma (hausdorff n X) hX.quadratic (q.radialFunction i) (q.radialFunction i) x ≤ B i)
    (hw : ∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
      (ball (q.center i) (S * q.radius i)) (w i))
    (hproj : ∀ i, SobolevSpace.restrictLp (hausdorff n X) hX.quadratic
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.RadialCompactnessSequence, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.restrictLp