SubsolutionSourceBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Controlling the potential term by a lower truncation level

theorem OAI.RegularPointCoordinates.upper_level_product_le line 13

theorem OAI.RegularPointCoordinates.integral_upper_level_mono line 37

Source documentation

Raising a nonnegative level decreases its quadratic tail energy.

theorem integral_upper_level_mono (u : SobolevSpace μ hQ) {j k : ℝ}
    (hj : 0 ≤ j) (hjk : j ≤ k) (A : Set X) :
    (∫ x in A, (max (SobolevSpace.toLp μ hQ u x-k) 0)^2 ∂μ) ≤
      ∫ x in A, (max (SobolevSpace.toLp μ hQ u x-j) 0)^2 ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.cutoff_upper_level_source_le line 55

Source documentation

Moving the cutoff test strictly above an earlier level absorbs the zeroth-order term into that earlier level's L² energy.

theorem cutoff_upper_level_source_le
    (u : SobolevSpace μ hQ) {j k : ℝ} (hj : 0 ≤ j) (hjk : j < k)
    {χ : X → ℝ} {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hb : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    {A : Set X} (hs : tsupport χ ⊆ A) :
    (∫ x, (χ x)^2*SobolevSpace.toLp μ hQ u x*
      max (SobolevSpace.toLp μ hQ u x-k) 0 ∂μ) ≤
      (k/(k-j))*(∫ x in A, (max (SobolevSpace.toLp μ hQ u x-j) 0)^2 ∂μ) := by
…

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