ProjectionLimitContradiction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal residuals retain their nonzero norm in the limit

theorem OAI.RegularPointCoordinates.PoissonHarmonicLimit.no_nonzero_orthogonal_euler_limit line 20

Source documentation

Once the actual equation has been passed to the Euclidean limit, the finite moments from the same compactness subsequence give the sharp projection contradiction. Any nonzero normalization is allowed.

theorem PoissonHarmonicLimit.no_nonzero_orthogonal_euler_limit
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    {S : ℝ} {p : ℕ → X} {r : ℕ → ℝ}
    {u : ℕ → Fin n → SobolevSpace (hausdorff n X) hX.quadratic}
    {V : ℕ → X → Euclidean n} {w f : ℕ → SobolevSpace (hausdorff n X) hX.quadratic}
    {model : EuclideanHarmonicModel n S} (hlimit : PoissonHarmonicLimit hX S p r u V w f model)
    (hS : 0 < S) {ρ : ℝ} (hρ : 0 < ρ) (hρS : ρ < S)
    (L : Euclidean n →L[ℝ] ℝ) (k : ℝ)
    (heuler : ∀ x ∈ ball 0 S, fderiv ℝ model.value x x = model.value x + L x + k)
    {c : ℝ} (hc : c ≠ 0)
    (hnorm : Tendsto (fun i =>
      ⟪localAffineMomentFamily (hausdorff n X) hX.quadratic (u i) (w i)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.PoissonHarmonicLimit, OAI.RegularPointCoordinates.localAffineMomentFamily