OAI/Geometry/RCD/Sobolev/DirichletTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absolute-value tails in the actual Dirichlet Sobolev space

  1. theorem OAI.RegularPointCoordinates.exists_dirichlet_absolute_tail line 17

    Source documentation

    Cutting off the absolute value below a nonnegative level preserves zero boundary values and does not increase Dirichlet energy.

    theorem exists_dirichlet_absolute_tail (Ω : Set X)
    (w : SobolevSpace.dirichlet μ hQ Ω) {t : ℝ} (ht : 0 ≤ t) :
    ∃ v : SobolevSpace.dirichlet μ hQ Ω,
      (SobolevSpace.toLp μ hQ v.val =ᵐ[μ]
        fun x => max (|SobolevSpace.toLp μ hQ w.val x|-t) 0) ∧
      energyForm μ hQ v.val v.val ≤ energyForm μ hQ w.val w.val := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm