Girsanov's theorem for a constant drift

Let W be a Brownian motion relative to a filtration ℱ under P, let θ : ℝ and T : ℝ≥0, and let Q = P.tilted (θ * W T ·), the probability measure with density exp (θ W_T - θ² T / 2) with respect to P. Then the process W^Q_t = W_t - θ min(t, T) is a Brownian motion relative to the same filtration ℱ, now under Q. On the horizon [0, T] it is W_t - θ t; with θ = -κ for a market price of risk κ it is W_t + κ t. After time T the density introduces no further drift: an increment of W starting at or after T keeps its law N(0, t - s) and its independence from the past under Q.

As Q is absolutely continuous with respect to P, almost surely continuous paths of W give almost surely continuous paths of W^Q, which is then a Brownian motion under Q in the sense of ProbabilityTheory.IsBrownianReal.

Main declarations

• TauCeti.Probability.IsFilteredPreBrownianReal.hasLaw_sub_tilted_mul_eval_of_horizon_le and TauCeti.Probability.IsFilteredPreBrownianReal.indep_sub_tilted_mul_eval_of_horizon_le: increments starting at or after the tilting horizon.
• TauCeti.Probability.IsFilteredPreBrownianReal.sub_mul_min_tilted_mul_eval: Girsanov's theorem for a constant drift.
• TauCeti.Probability.IsFilteredPreBrownianReal.isBrownianReal_sub_mul_min_tilted_mul_eval: the same statement for a Brownian motion with continuous paths.

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_of_horizon_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {s t T : NNReal} (hTs : T ≤ s) (hst : s ≤ 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 0 (t - s)) B

Once the tilting horizon T has passed, the density of the tilted measure is known: an event known at time s ≥ T and an event of the increment W t - W s factor, the latter with its original Gaussian probability.

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

An increment of W starting at or after the tilting horizon keeps its centered Gaussian law under the tilted measure.

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

An increment of W starting at or after the tilting horizon remains independent of the past under the tilted measure.

theorem TauCeti.Probability.IsFilteredPreBrownianReal.sub_mul_min_tilted_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) (T : NNReal) : IsFilteredPreBrownianReal ℱ (fun (t : NNReal) (ω : Ω) => W t ω - θ * ↑(min t T)) (P.tilted fun (ω : Ω) => θ * W T ω)

Girsanov's theorem for a constant drift. If W is a Brownian motion relative to ℱ under P, then t ↦ W t - θ min(t, T) is a Brownian motion relative to ℱ under the measure P.tilted (θ * W T ·), whose density with respect to P is exp (θ W_T - θ² T / 2).

theorem TauCeti.Probability.IsFilteredPreBrownianReal.isBrownianReal_sub_mul_min_tilted_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (hcont : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : NNReal) => W x ω) (θ : ℝ) (T : NNReal) : ProbabilityTheory.IsBrownianReal (fun (t : NNReal) (ω : Ω) => W t ω - θ * ↑(min t T)) (P.tilted fun (ω : Ω) => θ * W T ω)

Girsanov's theorem for a constant drift, with continuous paths. If moreover W has almost surely continuous paths, then t ↦ W t - θ min(t, T) is a Brownian motion under the measure P.tilted (θ * W T ·).