ActualEulerLimit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Passing the actual Sobolev Euler equation to the Euclidean limit

theorem OAI.RegularPointCoordinates.PoissonHarmonicLimit.euler_equation line 20

Source documentation

Joint compactness, the actual projected Sobolev equation, and a vanishing normalized error imply the limiting Euler equation. There is no assumption of an Euler equation for the limiting model.

theorem PoissonHarmonicLimit.euler_equation {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) (hV : ∀ i, Measurable (V i))
    (hrep : ∀ i j, SobolevSpace.toLp (hausdorff n X) hX.quadratic (u i j) =ᵐ[
      (hausdorff n X).restrict (ball (p i) (S * r i))] fun x => V i x j)
    (B : ℕ → ℝ)
    (hf : ∀ i, ∀ᵐ x ∂(hausdorff n X).restrict (ball (p i) (S * r i)),
      localGamma (hausdorff n X) hX.quadratic (f i) (f i) x ≤ B i)
    (e : ℕ → SobolevSpace (hausdorff n X) hX.quadratic)
…

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