OAI/Geometry/RCD/Sobolev/CutoffErrorLocalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.cutoff_error_on_le line 19

   Source documentation

   A cutoff between zero and one only decreases a local directional error.

   theorem cutoff_error_on_le (u : SobolevSpace μ hQ) (c : ℝ) (s : Set X) (hs : μ s ≠ ∞)
       {χ : X → ℝ} (hχ : AEStronglyMeasurable χ μ)
       (hχrange : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1) :
       (∫ x in s, χ x * |localGamma μ hQ u u x - c| ∂μ) ≤
         ∫ x in s, |localGamma μ hQ u u x - c| ∂μ := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

2. theorem OAI.RegularPointCoordinates.cutoff_error_integrable_of_finite_region line 35

   Source documentation

   Finite support measure suffices for integrability of the cutoff error.

   theorem cutoff_error_integrable_of_finite_region (u : SobolevSpace μ hQ) (c : ℝ)
       {s : Set X} (hs : μ s ≠ ∞) {χ : X → ℝ}
       (hχ : AEStronglyMeasurable χ μ) (hχrange : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
       (hχzero : ∀ x ∉ s, χ x = 0) :
       Integrable (fun x => χ x * |localGamma μ hQ u u x - c|) μ := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma

3. theorem OAI.RegularPointCoordinates.cutoff_error_on_le_total line 55

   Source documentation

   Every local portion of a cutoff error is bounded by its total error.

   theorem cutoff_error_on_le_total (u : SobolevSpace μ hQ) (c : ℝ)
       {s : Set X} (hs : μ s ≠ ∞) {χ : X → ℝ}
       (hχ : AEStronglyMeasurable χ μ) (hχrange : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
       (hχzero : ∀ x ∉ s, χ x = 0) (t : Set X) :
       (∫ x in t, χ x * |localGamma μ hQ u u x - c| ∂μ) ≤
         ∫ x, χ x * |localGamma μ hQ u u x - c| ∂μ :=
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma