OAI/Geometry/RCD/Sobolev/CutoffEnergyBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the actual compact energy density

  1. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoffEnergy_bound line 22

    Source documentation

    The true Sobolev product inherits the original directional gradient bound because the cutoff takes values in [0,1].

    theorem LocalHarmonicEnergy.cutoffEnergy_bound
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (hχ : ∀ z, 0 ≤ χ z ∧ χ z ≤ 1)
    (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ) :
    ∀ᵐ z ∂μ, |SobolevSpace.toLp μ hQ (G.cutoffEnergy μ hQ χ c) z| ≤
      (L : ℝ) ^ 2 * ‖v‖ ^ 2 := by
…

    Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp

  2. theorem OAI.RegularPointCoordinates.LocalHarmonicEnergy.cutoffEnergy_zero_off line 42

    Source documentation

    The compact density vanishes off any region containing the cutoff.

    theorem LocalHarmonicEnergy.cutoffEnergy_zero_off
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (χ : X →ᵇ ℝ) (c : SobolevSpace μ hQ) (hc : SobolevSpace.toLp μ hQ c =ᵐ[μ] χ)
    {A : Set X} (hzero : ∀ z ∉ A, χ z = 0) :
    ∀ᵐ z ∂μ, z ∉ A → SobolevSpace.toLp μ hQ (G.cutoffEnergy μ hQ χ c) z = 0 :=
…

    Mentions: OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp