AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2HorizonExtension

- Product-space prefix corresponding to times strictly before `T`.

def horizonPrefix (T : ℝ≥0) : Set (Omega × ℝ≥0) :=
  Set.univ ×ˢ Set.Iio T

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:30published source at 7bcd37294df1

No declaration docstring.

theorem measurableSet_horizonPrefix (T : ℝ≥0) :
    MeasurableSet (horizonPrefix (Omega := Omega) T) :=
  MeasurableSet.univ.prod measurableSet_Iio

/-- Restricting the larger process-time measure to the strict smaller prefix
recovers the smaller process-time measure exactly.  The only omitted point is
the terminal slice, which is time-null. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:33published source at 7bcd37294df1

- Restricting the larger process-time measure to the strict smaller prefix recovers the smaller process-time measure exactly. The only omitted point is the terminal slice, which is time-null.

theorem restrict_processTimeMeasure_horizonPrefix [SFinite mu]
    (hT : T₁ ≤ T₂) :
    (processTimeMeasure mu T₂).restrict (horizonPrefix (Omega := Omega) T₁) =
      processTimeMeasure mu T₁ := by
  rw [processTimeMeasure, processTimeMeasure, horizonPrefix,
    ← Measure.prod_restrict, Measure.restrict_univ,
    ← TimeMeasure.restrict_upTo_Iio_eq_of_le (T₁ := T₁) (T₂ := T₂) le_rfl hT,
    TimeMeasure.restrict_upTo_Iio_terminal]

/-- The product representative of deterministic zero extension is exactly the
indicator of the strict time prefix. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:40published source at 7bcd37294df1

- The product representative of deterministic zero extension is exactly the indicator of the strict time prefix.

theorem processFunction_restrictProcess_eq_indicator
    (eta : ℝ≥0 → Omega → ℝ) (T : ℝ≥0) :
    processFunction (ProgressiveL2Integrand.restrictProcess T eta) =
      (horizonPrefix (Omega := Omega) T).indicator (processFunction eta) := by
  funext z
  by_cases hz : z.2 < T
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess,
      horizonPrefix, hz]
  · simp [processFunction, ProgressiveL2Integrand.restrictProcess,
      horizonPrefix, hz]

/-- Extend a progressive `L²` integrand from `T₁` to `T₂ ≥ T₁` by zero after
`T₁`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:51published source at 7bcd37294df1

- Extend a progressive `L²` integrand from `T₁` to `T₂ ≥ T₁` by zero after `T₁`.

noncomputable def extendByZero [SFinite mu]
    (eta : ProgressiveL2Integrand filtration mu T₁) (hT : T₁ ≤ T₂) :
    ProgressiveL2Integrand filtration mu T₂ where
  process := ProgressiveL2Integrand.restrictProcess T₁ eta.process
  progressive := ProgressiveL2Integrand.restrictProcess_progressive eta T₁
  memLp := by
    rw [processFunction_restrictProcess_eq_indicator]
    apply (memLp_indicator_iff_restrict
      (measurableSet_horizonPrefix (Omega := Omega) T₁)).2
    rw [restrict_processTimeMeasure_horizonPrefix (mu := mu) hT]
    exact eta.memLp

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:64published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem extendByZero_process [SFinite mu]
    (eta : ProgressiveL2Integrand filtration mu T₁) (hT : T₁ ≤ T₂) :
    (extendByZero eta hT).process =
      ProgressiveL2Integrand.restrictProcess T₁ eta.process :=
  rfl

/-- Zero extension preserves the product-space `L²` norm exactly. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:76published source at 7bcd37294df1

- Zero extension preserves the product-space `L²` norm exactly.

theorem norm_extendByZero_eq [SFinite mu]
    (eta : ProgressiveL2Integrand filtration mu T₁) (hT : T₁ ≤ T₂) :
    ‖(extendByZero eta hT).toLp‖ = ‖eta.toLp‖ := by
  rw [ProgressiveL2Integrand.toLp, ProgressiveL2Integrand.toLp,
    Lp.norm_toLp, Lp.norm_toLp]
  rw [extendByZero_process,
    processFunction_restrictProcess_eq_indicator,
    eLpNorm_indicator_eq_eLpNorm_restrict
      (measurableSet_horizonPrefix (Omega := Omega) T₁),
    restrict_processTimeMeasure_horizonPrefix (mu := mu) hT]

/-- Zero extension commutes with subtraction in `L²`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:83published source at 7bcd37294df1

- Zero extension commutes with subtraction in `L²`.

theorem extendByZero_sub_toLp [SFinite mu]
    (eta xi : ProgressiveL2Integrand filtration mu T₁) (hT : T₁ ≤ T₂) :
    (extendByZero (sub eta xi) hT).toLp =
      (sub (extendByZero eta hT) (extendByZero xi hT)).toLp := by
  unfold ProgressiveL2Integrand.toLp
  apply MemLp.toLp_congr
  filter_upwards [] with z
  by_cases hz : z.2 < T₁
  · simp [extendByZero, ProgressiveL2Integrand.restrictProcess,
      sub, processFunction, hz]
  · simp [extendByZero, ProgressiveL2Integrand.restrictProcess,
      sub, processFunction, hz]

/-- Zero extension is an isometry for the product-space `L²` distance. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:95published source at 7bcd37294df1

- Zero extension is an isometry for the product-space `L²` distance.

theorem norm_extendByZero_sub_extendByZero_eq [SFinite mu]
    (eta xi : ProgressiveL2Integrand filtration mu T₁) (hT : T₁ ≤ T₂) :
    ‖(extendByZero eta hT).toLp - (extendByZero xi hT).toLp‖ =
      ‖eta.toLp - xi.toLp‖ := by
  rw [← toLp_sub, ← toLp_sub]
  rw [← extendByZero_sub_toLp eta xi hT]
  exact norm_extendByZero_eq (sub eta xi) hT

end ProgressiveL2HorizonExtension
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean:109published source at 7bcd37294df1