AutoSamplingTheory.TechnicalLemmas.Analysis.LeftLebesgueAverage

- Mean pointwise error over the left interval `[t-h,t]`.

noncomputable def leftAverageError (f : ℝ → ℝ) (t : ℝ) (h : ℝ≥0) : ℝ :=
  ⨍ s in Icc (t - (h : ℝ)) t, |f s - f t| ∂volume

AutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean:23published source at 77184245109a

No declaration docstring.

private theorem tendsto_sub_nhdsGT_zero_nhdsLT (t : ℝ) :
    Tendsto (fun h : ℝ ↦ t - h) (𝓝[>] 0) (𝓝[<] t) := by
  apply tendsto_nhdsWithin_iff.mpr
  constructor
  · have hfull : Tendsto (fun h : ℝ ↦ t - h) (𝓝 0) (𝓝 t) := by
      simpa using ((tendsto_const_nhds :
        Tendsto (fun _ : ℝ ↦ t) (𝓝 (0 : ℝ)) (𝓝 t)).sub tendsto_id)
    exact hfull.mono_left
      (show (𝓝[>] (0 : ℝ)) ≤ 𝓝 0 from inf_le_left)
  · filter_upwards [self_mem_nhdsWithin] with h hh
    exact sub_lt_self t hh

AutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean:26published source at 77184245109a

No declaration docstring.

private theorem ae_tendsto_leftAverageError_real
    {f : ℝ → ℝ} (hf : LocallyIntegrable f volume) :
    ∀ᵐ t ∂volume,
      Tendsto (fun h : ℝ ↦ ⨍ s in Icc (t - h) t, |f s - f t| ∂volume)
        (𝓝[>] 0) (𝓝 0) := by
  have hdiff := (vitaliFamily volume 1).ae_tendsto_average_norm_sub hf
  filter_upwards [hdiff] with t ht
  have hsets :
      Tendsto (fun h : ℝ ↦ Icc (t - h) t) (𝓝[>] 0)
        ((vitaliFamily volume 1).filterAt t) :=
    t.tendsto_Icc_vitaliFamily_left.comp (tendsto_sub_nhdsGT_zero_nhdsLT t)
  change Tendsto
    ((fun a : Set ℝ ↦ ⨍ s in a, |f s - f t| ∂volume) ∘
      fun h : ℝ ↦ Icc (t - h) t) (𝓝[>] 0) (𝓝 0)
  simpa only [Real.norm_eq_abs] using ht.comp hsets

/-- For almost every time, the left average error converges to zero as a
strictly positive nonnegative window shrinks to zero. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean:38published source at 77184245109a

- For almost every time, the left average error converges to zero as a strictly positive nonnegative window shrinks to zero.

theorem ae_tendsto_leftAverageError
    {f : ℝ → ℝ} (hf : LocallyIntegrable f volume) :
    ∀ᵐ t ∂volume,
      Tendsto (fun h : ℝ≥0 ↦ leftAverageError f t h)
        (𝓝[>] 0) (𝓝 0) := by
  filter_upwards [ae_tendsto_leftAverageError_real hf] with t ht
  have hcoe :
      Tendsto ((↑) : ℝ≥0 → ℝ) (𝓝[>] 0) (𝓝[>] 0) := by
    show Filter.map ((↑) : ℝ≥0 → ℝ) (𝓝[>] 0) ≤ 𝓝[>] (0 : ℝ)
    rw [NNReal.map_coe_nhdsGT]
    simp
  change Tendsto
    ((fun h : ℝ ↦ ⨍ s in Icc (t - h) t, |f s - f t| ∂volume) ∘
      ((↑) : ℝ≥0 → ℝ)) (𝓝[>] 0) (𝓝 0)
  exact ht.comp hcoe

/-- Sequential form used by dyadic meshes: any positive real mesh tending to
zero gives vanishing left average error along twice that mesh. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean:56published source at 77184245109a

- Sequential form used by dyadic meshes: any positive real mesh tending to zero gives vanishing left average error along twice that mesh.

theorem ae_tendsto_leftAverageError_two_mul
    {f : ℝ → ℝ} (hf : LocallyIntegrable f volume)
    {mesh : ℕ → ℝ} (hmesh : Tendsto mesh atTop (𝓝 0))
    (hmeshPos : ∀ n, 0 < mesh n) :
    ∀ᵐ t ∂volume,
      Tendsto
        (fun n ↦ leftAverageError f t
          ⟨2 * mesh n, (mul_pos (by norm_num) (hmeshPos n)).le⟩)
        atTop (𝓝 0) := by
  let widths : ℕ → ℝ≥0 :=
    fun n ↦ ⟨2 * mesh n, (mul_pos (by norm_num) (hmeshPos n)).le⟩
  have hwidths_nhds : Tendsto widths atTop (𝓝 (0 : ℝ≥0)) := by
    apply NNReal.tendsto_coe.mp
    change Tendsto (fun n ↦ (2 : ℝ) * mesh n) atTop (𝓝 (0 : ℝ))
    simpa using
      (tendsto_const_nhds.mul hmesh :
        Tendsto (fun n ↦ (2 : ℝ) * mesh n) atTop (𝓝 (2 * 0)))
  have hwidths : Tendsto widths atTop (𝓝[>] (0 : ℝ≥0)) := by
    apply tendsto_nhdsWithin_iff.mpr
    refine ⟨hwidths_nhds, ?_⟩
    filter_upwards [] with n
    exact (mul_pos (by norm_num) (hmeshPos n))
  filter_upwards [ae_tendsto_leftAverageError hf] with t ht
  change Tendsto (fun n ↦ leftAverageError f t (widths n)) atTop (𝓝 0)
  exact ht.comp hwidths

/-- A normalized average on a subinterval of the left neighborhood has error
at most twice the full-neighborhood average when its mass is half the mass of
the neighborhood.  This is the deterministic estimate behind one-cell-lagged
dyadic convergence. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean:74published source at 77184245109a

- A normalized average on a subinterval of the left neighborhood has error at most twice the full-neighborhood average when its mass is half the mass of the neighborhood. This is the deterministic estimate behind one-cell-lagged dyadic convergence.

theorem abs_normalized_setIntegral_sub_le_two_mul_leftAverageError
    {f : ℝ → ℝ} (hf : LocallyIntegrable f volume)
    {a b t delta : ℝ} (hdelta : 0 < delta)
    (hab : b - a = delta)
    (hsubset : Ioc a b ⊆ Icc (t - 2 * delta) t) :
    |delta⁻¹ * ∫ s in Ioc a b, f s ∂volume - f t| ≤
      2 * ⨍ s in Icc (t - 2 * delta) t, |f s - f t| ∂volume := by
  have hab_le : a ≤ b := sub_nonneg.mp (hab.symm ▸ hdelta.le)
  have hbig_le : t - 2 * delta ≤ t := sub_le_self _ (by positivity)
  have hf_big : IntegrableOn f (Icc (t - 2 * delta) t) volume :=
    hf.integrableOn_isCompact isCompact_Icc
  have hconst_big : IntegrableOn (fun _ : ℝ ↦ f t)
      (Icc (t - 2 * delta) t) volume :=
    continuous_const.integrableOn_Icc
  have herror_big : IntegrableOn (fun s ↦ |f s - f t|)
      (Icc (t - 2 * delta) t) volume :=
    (hf_big.sub hconst_big).abs
  have hf_small : IntegrableOn f (Ioc a b) volume :=
    hf_big.mono_set hsubset
  have hconst_small : IntegrableOn (fun _ : ℝ ↦ f t) (Ioc a b) volume :=
    continuous_const.integrableOn_Ioc
  have hmass_small : volume.real (Ioc a b) = delta := by
    rw [Real.volume_real_Ioc_of_le hab_le, hab]
  have hmass_big : volume.real (Icc (t - 2 * delta) t) = 2 * delta := by
    rw [Real.volume_real_Icc_of_le hbig_le]
    ring
  have hconst_average :
      delta⁻¹ * ∫ _s in Ioc a b, f t ∂volume = f t := by
    rw [integral_const, measureReal_restrict_apply_univ, hmass_small]
    simp only [smul_eq_mul]
    field_simp
  have hrewrite :
      delta⁻¹ * ∫ s in Ioc a b, f s ∂volume - f t =
        delta⁻¹ * ∫ s in Ioc a b, (f s - f t) ∂volume := by
    have hisub :
        ∫ s in Ioc a b, (f s - f t) ∂volume =
          (∫ s in Ioc a b, f s ∂volume) -
            ∫ _s in Ioc a b, f t ∂volume :=
      integral_sub hf_small hconst_small
    calc
      delta⁻¹ * ∫ s in Ioc a b, f s ∂volume - f t =
          delta⁻¹ * ∫ s in Ioc a b, f s ∂volume -
            delta⁻¹ * ∫ _s in Ioc a b, f t ∂volume :=
        congrArg (fun x ↦ delta⁻¹ * ∫ s in Ioc a b, f s ∂volume - x)
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean:104published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.