Brownian increments under a terminal exponential tilt

Let W be Brownian relative to a filtration ℱ. Under the probability measure Q = P.tilted (θ * W T ·), every increment W t - W s, for s ≤ t ≤ T, has law N(θ (t - s), t - s) and is independent of ℱ s. Thus the increments of W t - θ t are centered Gaussian and independent of the past on the whole finite horizon. Taking θ = -κ gives the drift correction W t + κ t.

The transition formula on a past event is also exported. It uses the density at time t and the independence under P to separate the past density from the increment density. Exponential tilting of the scalar Gaussian identifies the latter factor. No assertion about times beyond T is made.

References

• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §3.5.
• S. E. Shreve, Stochastic Calculus for Finance II: Continuous-Time Models, Springer, 2004, §5.2.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.tilted_mul_eval_inter_preimage {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {s t T : NNReal} (hst : s ≤ t) (htT : t ≤ T) {A : Set Ω} (hA : MeasurableSet A) {B : Set ℝ} (hB : MeasurableSet B) : (P.tilted fun (ω : Ω) => θ * W T ω) (A ∩ (W t - W s) ⁻¹' B) = (P.tilted fun (ω : Ω) => θ * W T ω) A * (ProbabilityTheory.gaussianReal (θ * (↑t - ↑s)) (t - s)) B

Under a terminal exponential tilt, the probability of an increment event and an event known at its starting time factors through the shifted Gaussian transition law.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.hasLaw_sub_tilted_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {s t T : NNReal} (hst : s ≤ t) (htT : t ≤ T) : ProbabilityTheory.HasLaw (W t - W s) (ProbabilityTheory.gaussianReal (θ * (↑t - ↑s)) (t - s)) (P.tilted fun (ω : Ω) => θ * W T ω)

On the tilting horizon, a Brownian increment acquires mean θ (t - s) and retains variance t - s. The statement includes zero-length increments.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.indep_sub_tilted_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {s t T : NNReal} (hst : s ≤ t) (htT : t ≤ T) : ProbabilityTheory.Indep (MeasurableSpace.comap (W t - W s) inferInstance) (↑ℱ s) (P.tilted fun (ω : Ω) => θ * W T ω)

Brownian increments remain independent of the past under the terminal exponential tilt, provided the increment ends no later than the tilting horizon.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.hasLaw_sub_drift_tilted_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {s t T : NNReal} (hst : s ≤ t) (htT : t ≤ T) : ProbabilityTheory.HasLaw (fun (ω : Ω) => W t ω - θ * ↑t - (W s ω - θ * ↑s)) (ProbabilityTheory.gaussianReal 0 (t - s)) (P.tilted fun (ω : Ω) => θ * W T ω)

Subtracting the acquired drift centers every increment under the terminal tilt. With θ = -κ this is the Gaussian increment law of W t + κ t on [0,T].

theorem TauCeti.Probability.IsFilteredPreBrownianReal.indep_sub_drift_tilted_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {s t T : NNReal} (hst : s ≤ t) (htT : t ≤ T) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun (ω : Ω) => W t ω - θ * ↑t - (W s ω - θ * ↑s)) inferInstance) (↑ℱ s) (P.tilted fun (ω : Ω) => θ * W T ω)

The drift-corrected increments are independent of the original filtration's past.