Comparing the early cutoff error with trace mass #
The time derivative of the lower cutoff contributes only on its transition strip. A nonnegative majorant there is integrated over the larger trace cylinder.
theorem
ESS.bu_short_early_integral_le_trace
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
{K S : Set X}
(hKmeas : MeasurableSet K)
(hSmeas : MeasurableSet S)
{f g : X → ℝ}
(hf : MeasureTheory.IntegrableOn f S μ)
(hg : MeasureTheory.IntegrableOn g K μ)
(hf0 : ∀ (z : X), 0 ≤ f z)
(C : ℝ)
(hC : 0 ≤ C)
(hbound : ∀ z ∈ K, g z ≤ C * S.indicator f z)
:
An integrable error supported on a measurable strip is bounded by a nonnegative majorant integrated over the full strip.
theorem
ESS.bu_short_closed_strip_scaled_tendsto_zero
(B : Set CKN.Foundation.Parabolic.Vec3)
(f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(C : ℝ)
(htrace :
Filter.Tendsto
(fun (ε : ℝ) =>
(∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ Set.Ioc (1 / 2 + ε) (1 / 2 + 2 * ε), f q) / ε ^ 2)
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0))
:
Replacing the half-open shrinking strip by its closed version does not change its integral, and a fixed coefficient preserves the trace limit.