AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LocalProgressiveL2

- A progressive process whose squared time integral on `[0,T]` is finite almost surely. No finite expected energy is assumed.

structure LocalProgressiveL2Integrand
    (filtration : Filtration ℝ≥0 m) (mu : Measure Omega) (T : ℝ≥0) where
  process : ℝ≥0 → Omega → ℝ
  progressive : IsStronglyProgressive filtration process
  finiteEnergy : IsLocallySquareIntegrableOn process mu T

/-- Zero extension of the squared process from `[0,b] × Ω`.  The sample-space
measurable structure is the filtration at `b`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:28published source at 77184245109a

- Zero extension of the squared process from `[0,b] × Ω`. The sample-space measurable structure is the filtration at `b`.

noncomputable def squaredExtensionAt
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (b : ℝ≥0) : ℝ≥0 × Omega → ℝ :=
  Function.extend
    (Prod.map ((↑) : Set.Iic b → ℝ≥0) id)
    (fun p : Set.Iic b × Omega => (eta.process p.1 p.2) ^ 2)
    0

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:36published source at 77184245109a

No declaration docstring.

theorem squaredExtensionAt_stronglyMeasurable
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (b : ℝ≥0) :
    @StronglyMeasurable (ℝ≥0 × Omega) ℝ inferInstance
      (MeasurableSpace.prod inferInstance (filtration b))
      (squaredExtensionAt eta b) := by
  apply ((MeasurableEmbedding.subtype_coe measurableSet_Iic).prodMap
    MeasurableEmbedding.id).stronglyMeasurable_extend
  · exact (eta.progressive b).pow 2
  · exact stronglyMeasurable_const

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:44published source at 77184245109a

No declaration docstring.

@[simp] theorem squaredExtensionAt_apply_of_le
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {s b : ℝ≥0} (hsb : s ≤ b) (omega : Omega) :
    squaredExtensionAt eta b (s, omega) = (eta.process s omega) ^ 2 := by
  let p : Set.Iic b × Omega := (⟨s, hsb⟩, omega)
  exact ((MeasurableEmbedding.subtype_coe measurableSet_Iic).prodMap
    MeasurableEmbedding.id).injective.extend_apply
      (fun q : Set.Iic b × Omega => (eta.process q.1 q.2) ^ 2) 0 p

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:55published source at 77184245109a

No declaration docstring.

@[simp] theorem squaredExtensionAt_apply_of_not_le
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {s b : ℝ≥0} (hsb : ¬s ≤ b) (omega : Omega) :
    squaredExtensionAt eta b (s, omega) = 0 := by
  rw [squaredExtensionAt, Function.extend_apply']
  · rfl
  · rintro ⟨u, hu⟩
    apply hsb
    have hsu := congrArg Prod.fst hu
    change (u.1 : ℝ≥0) = s at hsu
    have hub : (u.1 : ℝ≥0) ≤ b := u.1.property
    rwa [hsu] at hub

/-- Real-valued accumulated energy.  On the almost-sure finite-energy set it
agrees with the exact `ENNReal` accumulated energy and is continuous in time;
those comparison and continuity statements are proved downstream. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:64published source at 77184245109a

- Real-valued accumulated energy. On the almost-sure finite-energy set it agrees with the exact `ENNReal` accumulated energy and is continuous in time; those comparison and continuity statements are proved downstream.

noncomputable def accumulatedEnergyReal
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (t : ℝ≥0) (omega : Omega) : ℝ :=
  ∫ s, squaredExtensionAt eta (min t T) (s, omega)
    ∂(TimeMeasure.upTo T)

/-- At each fixed time the real energy is measurable with respect to the
filtration at the stopped time `min t T`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:80published source at 77184245109a

- At each fixed time the real energy is measurable with respect to the filtration at the stopped time `min t T`.

theorem accumulatedEnergyReal_stronglyMeasurable
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (t : ℝ≥0) :
    StronglyMeasurable[filtration (min t T)]
      (accumulatedEnergyReal eta t) := by
  exact @StronglyMeasurable.integral_prod_left'
    ℝ≥0 Omega ℝ inferInstance (filtration (min t T))
    (TimeMeasure.upTo T) inferInstance inferInstance inferInstance
    (squaredExtensionAt eta (min t T))
    (squaredExtensionAt_stronglyMeasurable eta (min t T))

/-- Fixed-time energy is measurable in the ambient sample sigma-algebra. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:88published source at 77184245109aOpen detailed card

- Fixed-time energy is measurable in the ambient sample sigma-algebra.

theorem accumulatedEnergyReal_stronglyMeasurable_ambient
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (t : ℝ≥0) :
    StronglyMeasurable (accumulatedEnergyReal eta t) :=
  (accumulatedEnergyReal_stronglyMeasurable eta t).mono
    (filtration.le (min t T))

end LocalProgressiveL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean:100published source at 77184245109a