EulerForcing.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar forcing in the local Euler equation

theorem OAI.RegularPointCoordinates.LocalMeanPoincareInput.euler_forcing line 17

Source documentation

Local Poincare turns the gradient estimate for Gamma(f,v)-v into an actual scalar Euler equation with a constant and an L2 error. The error has a global Sobolev representative, ready for the transport test.

theorem LocalMeanPoincareInput.euler_forcing {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalMeanPoincareInput hX) {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
      ∀ (f v G η : SobolevSpace (hausdorff n X) hX.quadratic),
      (SobolevSpace.toLp (hausdorff n X) hX.quadratic G =ᵐ[
        (hausdorff n X).restrict (ball p R)] localGamma (hausdorff n X) hX.quadratic f v) →
      (SobolevSpace.toLp (hausdorff n X) hX.quadratic η =ᵐ[
        (hausdorff n X).restrict (ball p R)] fun _ => (1 : ℝ)) →
      ∃ (k : ℝ) (e : SobolevSpace (hausdorff n X) hX.quadratic),
        localGamma (hausdorff n X) hX.quadratic f v =ᵐ[
          (hausdorff n X).restrict (ball p R)]
          (fun x => SobolevSpace.toLp (hausdorff n X) hX.quadratic v x + k +
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalMeanPoincareInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma