Documentation

LeanPool.EscauriazaSereginSverak.LPS.ContinuationCutoff

Smooth time cutoffs at a slab endpoint #

A monotone smooth cutoff equal to one before b - 2ε and to zero after b - ε. Testing a weak formulation against such cutoffs exhibits the boundary term at the slab endpoint (lem:lps-continuation).

source
noncomputable def ESS.lpsCutoffRight (b ε t : ℝ) :
ℝ

The smooth cutoff 1 on (-∞, b - 2ε] and 0 on [b - ε, ∞).

Equations
Instances For
    source
    theorem ESS.lpsCutoffRight_contDiff (b ε : ℝ) :
    ContDiff ℝ (↑⊤) (lpsCutoffRight b ε)
    source
    theorem ESS.lpsCutoffRight_eq_one {b ε t : ℝ} (hε : 0 < ε) (ht : t ≤ b - 2 * ε) :
    lpsCutoffRight b ε t = 1
    source
    theorem ESS.lpsCutoffRight_eq_zero {b ε t : ℝ} (hε : 0 < ε) (ht : b - ε ≤ t) :
    lpsCutoffRight b ε t = 0
    source
    theorem ESS.lpsCutoffRight_nonneg (b ε t : ℝ) :
    0 ≤ lpsCutoffRight b ε t
    source
    theorem ESS.lpsCutoffRight_le_one (b ε t : ℝ) :
    lpsCutoffRight b ε t ≤ 1
    source
    theorem ESS.lpsCutoffRight_antitone {b ε : ℝ} (hε : 0 < ε) :
    Antitone (lpsCutoffRight b ε)
    source
    theorem ESS.deriv_lpsCutoffRight_nonpos {b ε : ℝ} (hε : 0 < ε) (t : ℝ) :
    deriv (lpsCutoffRight b ε) t ≤ 0
    source
    theorem ESS.deriv_lpsCutoffRight_eq_zero_of_le {b ε t : ℝ} (hε : 0 < ε) (ht : t < b - 2 * ε) :
    deriv (lpsCutoffRight b ε) t = 0
    source
    theorem ESS.deriv_lpsCutoffRight_eq_zero_of_ge {b ε t : ℝ} (hε : 0 < ε) (ht : b - ε < t) :
    deriv (lpsCutoffRight b ε) t = 0
    source
    theorem ESS.lps_endpoint_boundary_right {a b ℓ : ℝ} (hab : a < b) {F1 F2 : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF1 : MeasureTheory.Integrable F1 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))) (hF2 : MeasureTheory.Integrable F2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))) (hid : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), lpsCutoffRight b ε q.2 * F1 q - deriv (lpsCutoffRight b ε) q.2 * F2 q ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)) = 0) (hG : ∀ δ > 0, ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), b - η < t → |(∫ (x : CKN.Foundation.Parabolic.Vec3), F2 (x, t)) - ℓ| < δ) :
    ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), F1 q ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)) = -ℓ

    Boundary term at the right end of a slab: if the cutoff-tested identity ∫ η_ε F₁ - ∫ η_ε' F₂ = 0 holds for all small ε and the time profile t ↦ ∫ F₂(·, t) tends to ℓ at b from the left, then ∫ F₁ = -ℓ (lem:lps-continuation).

    source
    noncomputable def ESS.lpsCutoffLeft (a ε t : ℝ) :
    ℝ

    The smooth cutoff 0 on (-∞, a + ε] and 1 on [a + 2ε, ∞), obtained by reflecting the right-end cutoff.

    Equations
    Instances For
      source
      theorem ESS.lpsCutoffLeft_contDiff (a ε : ℝ) :
      ContDiff ℝ (↑⊤) (lpsCutoffLeft a ε)
      source
      theorem ESS.lpsCutoffLeft_eq_zero {a ε t : ℝ} (hε : 0 < ε) (ht : t ≤ a + ε) :
      lpsCutoffLeft a ε t = 0
      source
      theorem ESS.lpsCutoffLeft_eq_one {a ε t : ℝ} (hε : 0 < ε) (ht : a + 2 * ε ≤ t) :
      lpsCutoffLeft a ε t = 1
      source
      theorem ESS.lpsCutoffLeft_nonneg (a ε t : ℝ) :
      0 ≤ lpsCutoffLeft a ε t
      source
      theorem ESS.lpsCutoffLeft_le_one (a ε t : ℝ) :
      lpsCutoffLeft a ε t ≤ 1
      source
      theorem ESS.deriv_lpsCutoffLeft_eq_zero_of_le {a ε t : ℝ} (hε : 0 < ε) (ht : t < a + ε) :
      deriv (lpsCutoffLeft a ε) t = 0
      source
      theorem ESS.deriv_lpsCutoffLeft_eq_zero_of_ge {a ε t : ℝ} (hε : 0 < ε) (ht : a + 2 * ε < t) :
      deriv (lpsCutoffLeft a ε) t = 0
      source
      theorem ESS.lps_endpoint_boundary_left {a b ℓ : ℝ} (hab : a < b) {F1 F2 : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF1 : MeasureTheory.Integrable F1 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))) (hF2 : MeasureTheory.Integrable F2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))) (hid : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), lpsCutoffLeft a ε q.2 * F1 q - deriv (lpsCutoffLeft a ε) q.2 * F2 q ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)) = 0) (hG : ∀ δ > 0, ∃ η > 0, ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), t < a + η → |(∫ (x : CKN.Foundation.Parabolic.Vec3), F2 (x, t)) - ℓ| < δ) :
      ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), F1 q ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)) = ℓ

      Boundary term at the left end of a slab: if the cutoff-tested identity ∫ η_ε F₁ - ∫ η_ε' F₂ = 0 holds for all small ε with the left cutoffs and the time profile t ↦ ∫ F₂(·, t) tends to ℓ at a from the right, then ∫ F₁ = ℓ (lem:lps-continuation).