AutoSamplingTheory.TechnicalLemmas.Analysis.PrefixIntegral

- Prefix integral on the finite nonnegative-time horizon.

noncomputable def prefixIntegral
    (f : ℝ≥0 → ℝ) (T t : ℝ≥0) : ℝ :=
  ∫ s, if s < min t T then f s else 0 ∂(TimeMeasure.upTo T)

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:24published source at 77184245109a

No declaration docstring.

@[simp] theorem prefixIntegral_zero (f : ℝ≥0 → ℝ) (T : ℝ≥0) :
    prefixIntegral f T 0 = 0 := by
  simp [prefixIntegral]

/-- The moving-prefix integrand is the indicator of an initial interval. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:28published source at 77184245109a

- The moving-prefix integrand is the indicator of an initial interval.

private theorem prefixIntegrand_eq_indicator
    (f : ℝ≥0 → ℝ) (T t : ℝ≥0) :
    (fun s => if s < min t T then f s else 0) =
      (Iio (min t T)).indicator f := by
  funext s
  simp only [Set.indicator, Set.mem_Iio]

/-- Prefix integration is an ordinary set integral over the active initial
interval.  This representation exposes the exact measure restriction needed
for cross-horizon consistency. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:33published source at 77184245109a

- Prefix integration is an ordinary set integral over the active initial interval. This representation exposes the exact measure restriction needed for cross-horizon consistency.

theorem prefixIntegral_eq_setIntegral
    (f : ℝ≥0 → ℝ) (T t : ℝ≥0) :
    prefixIntegral f T t =
      ∫ s in Iio (min t T), f s ∂(TimeMeasure.upTo T) := by
  rw [prefixIntegral, prefixIntegrand_eq_indicator]
  exact integral_indicator measurableSet_Iio

/-- An earlier prefix integral is independent of which larger finite horizon is
used as the ambient truncation container. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:43published source at 77184245109a

- An earlier prefix integral is independent of which larger finite horizon is used as the ambient truncation container.

theorem prefixIntegral_eq_of_le_horizons
    (f : ℝ≥0 → ℝ) {t T₁ T₂ : ℝ≥0}
    (ht : t ≤ T₁) (hT : T₁ ≤ T₂) :
    prefixIntegral f T₁ t = prefixIntegral f T₂ t := by
  rw [prefixIntegral_eq_setIntegral, prefixIntegral_eq_setIntegral,
    min_eq_left ht, min_eq_left (ht.trans hT)]
  change
    ∫ s, f s ∂((TimeMeasure.upTo T₁).restrict (Iio t)) =
      ∫ s, f s ∂((TimeMeasure.upTo T₂).restrict (Iio t))
  rw [TimeMeasure.restrict_upTo_Iio_eq_of_le ht hT]

/-- The prefix integral is continuous in its upper time argument. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:52published source at 77184245109a

- The prefix integral is continuous in its upper time argument.

theorem continuous_prefixIntegral
    {f : ℝ≥0 → ℝ} {T : ℝ≥0}
    (hf : Integrable f (TimeMeasure.upTo T)) :
    Continuous (prefixIntegral f T) := by
  rw [continuous_iff_continuousAt]
  intro t0
  let g : ℝ≥0 → ℝ≥0 → ℝ := fun t s =>
    if s < min t T then f s else 0
  have hmeas : ∀ᶠ t in 𝓝 t0,
      AEStronglyMeasurable (g t) (TimeMeasure.upTo T) := by
    filter_upwards [] with t
    have hind := hf.1.indicator
      (measurableSet_Iio : MeasurableSet (Iio (min t T)))
    simpa only [g, prefixIntegrand_eq_indicator] using hind
  have hbound : ∀ᶠ t in 𝓝 t0,
      ∀ᵐ s ∂(TimeMeasure.upTo T), ‖g t s‖ ≤ ‖f s‖ := by
    filter_upwards [] with t
    filter_upwards [] with s
    by_cases hs : s < min t T
    · simp only [g, if_pos hs]
      exact le_rfl
    · simp only [g, if_neg hs, norm_zero]
      exact norm_nonneg _
  have hneq : ∀ᵐ s ∂(TimeMeasure.upTo T), s ≠ min t0 T := by
    rw [ae_iff]
    simpa using TimeMeasure.upTo_singleton T (min t0 T)
  have hb : Tendsto (fun t : ℝ≥0 => min t T) (𝓝 t0) (𝓝 (min t0 T)) :=
    continuousAt_id.min continuousAt_const
  have hpoint : ∀ᵐ s ∂(TimeMeasure.upTo T),
      Tendsto (fun t => g t s) (𝓝 t0) (𝓝 (g t0 s)) := by
    filter_upwards [hneq] with s hs
    by_cases hslt : s < min t0 T
    · have hev : ∀ᶠ t in 𝓝 t0, s < min t T :=
        (tendsto_order.1 hb).1 s hslt
      have heq : (fun t => g t s) =ᶠ[𝓝 t0]
          (fun _ : ℝ≥0 => f s) := by
        filter_upwards [hev] with t ht
        simp only [g, if_pos ht]
      rw [show g t0 s = f s by simp only [g, if_pos hslt]]
      exact (tendsto_congr' heq).2 tendsto_const_nhds
    · have hle : min t0 T ≤ s := le_of_not_gt hslt
      have hlt : min t0 T < s := lt_of_le_of_ne hle hs.symm
      have hev : ∀ᶠ t in 𝓝 t0, min t T < s :=
        (tendsto_order.1 hb).2 s hlt
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:64published source at 77184245109aOpen detailed card

Excerpt truncated; the exact source link is authoritative.

- Prefix integration is monotone in time for pointwise nonnegative integrands.

theorem prefixIntegral_mono
    {f : ℝ≥0 → ℝ} {T s t : ℝ≥0}
    (hf : Integrable f (TimeMeasure.upTo T))
    (hnonneg : ∀ u, 0 ≤ f u) (hst : s ≤ t) :
    prefixIntegral f T s ≤ prefixIntegral f T t := by
  unfold prefixIntegral
  have hs : Integrable (fun u => if u < min s T then f u else 0)
      (TimeMeasure.upTo T) := by
    rw [prefixIntegrand_eq_indicator]
    exact hf.indicator measurableSet_Iio
  have ht : Integrable (fun u => if u < min t T then f u else 0)
      (TimeMeasure.upTo T) := by
    rw [prefixIntegrand_eq_indicator]
    exact hf.indicator measurableSet_Iio
  apply integral_mono hs ht
  intro u
  have hmin : min s T ≤ min t T := min_le_min hst le_rfl
  by_cases hu : u < min s T
  · have hut : u < min t T := hu.trans_le hmin
    simp only [if_pos hu, if_pos hut]
    exact le_rfl
  · by_cases hut : u < min t T
    · simp only [if_neg hu, if_pos hut]
      exact hnonneg u
    · simp only [if_neg hu, if_neg hut]
      exact le_rfl

/-- Prefix integration stabilizes once the observation time passes the
terminal horizon. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:122published source at 77184245109a

- Prefix integration stabilizes once the observation time passes the terminal horizon.

theorem prefixIntegral_eq_terminal_of_le
    (f : ℝ≥0 → ℝ) (T t : ℝ≥0) (hTt : T ≤ t) :
    prefixIntegral f T t = prefixIntegral f T T := by
  simp only [prefixIntegral, min_eq_right hTt, min_self]

end PrefixIntegral
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean:151published source at 77184245109a