Documentation

TauCeti.Probability.BrownianMotion.ExponentialMartingale

The exponential martingale of a Brownian motion #

For a real parameter θ and a Brownian motion W, the process

Z_t = exp (θ W_t - θ² t / 2)

(TauCeti.Probability.exponentialMartingale θ W) is a strictly positive martingale with E[Z_t] = 1, relative to every filtration for which W is a Brownian motion. It is the density process of the change of measure in Girsanov's theorem: tilting the reference measure P by θ W_T, that is dQ = Z_T dP, gives a probability measure equivalent to P, and on the events known at time t ≤ T this measure has density Z_t. With θ = -κ for a market price of risk κ, Q is the candidate for the risk-neutral measure of the Black–Scholes market; identifying it as such requires Girsanov's theorem and the martingale property of discounted prices under Q, which are not proved here.

Brownian motion relative to a filtration is TauCeti.Probability.IsFilteredPreBrownianReal, from TauCeti.Probability.BrownianMotion.Filtered.

Main declarations #

References #

source
noncomputable def TauCeti.Probability.exponentialMartingale {Ω : Type u_1} (θ : ℝ) (W : NNReal → Ω → ℝ) (t : NNReal) (ω : Ω) :
ℝ

The exponential martingale exp (θ W_t - θ² t / 2) of a Brownian motion W with parameter θ.

Instances For
    source
    theorem TauCeti.Probability.exponentialMartingale_def {Ω : Type u_1} (θ : ℝ) (W : NNReal → Ω → ℝ) (t : NNReal) (ω : Ω) :
    exponentialMartingale θ W t ω = Real.exp (θ * W t ω - θ ^ 2 * ↑t / 2)

    Unfolding lemma for exponentialMartingale.

    source
    theorem TauCeti.Probability.exponentialMartingale_pos {Ω : Type u_1} (θ : ℝ) (W : NNReal → Ω → ℝ) (t : NNReal) (ω : Ω) :
    0 < exponentialMartingale θ W t ω

    The exponential martingale is strictly positive.

    source
    @[simp]
    theorem TauCeti.Probability.exponentialMartingale_zero_left {Ω : Type u_1} (W : NNReal → Ω → ℝ) :
    exponentialMartingale 0 W = 1

    With parameter 0 the exponential martingale is constantly 1.

    source
    theorem TauCeti.Probability.exponentialMartingale_eq_mul {Ω : Type u_1} (θ : ℝ) (W : NNReal → Ω → ℝ) (s t : NNReal) (ω : Ω) :
    exponentialMartingale θ W t ω = exponentialMartingale θ W s ω * Real.exp (θ * (W t ω - W s ω) - θ ^ 2 * (↑t - ↑s) / 2)

    From time s to time t ≥ s the exponential martingale is multiplied by the exponential of the increment θ (W_t - W_s) - θ² (t - s) / 2.

    source
    theorem TauCeti.Probability.rpow_exponentialMartingale {Ω : Type u_1} (θ q : ℝ) (W : NNReal → Ω → ℝ) (t : NNReal) (ω : Ω) :
    exponentialMartingale θ W t ω ^ q = Real.exp (q * (q - 1) * θ ^ 2 * ↑t / 2) * exponentialMartingale (q * θ) W t ω

    A real power of the exponential martingale is a deterministic multiple of the exponential martingale with the scaled parameter: Z^θ_t ^ q = exp (q (q - 1) θ² t / 2) * Z^{qθ}_t.

    source
    theorem MeasureTheory.Adapted.stronglyAdapted_exponentialMartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ℱ : Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : Adapted ℱ W) (θ : ℝ) :
    StronglyAdapted ℱ (TauCeti.Probability.exponentialMartingale θ W)

    The exponential martingale of a process adapted to ℱ is adapted to ℱ.

    source
    theorem ProbabilityTheory.IsPreBrownianReal.integrable_exp_mul_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (θ : ℝ) (t : NNReal) :
    MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (θ * B t ω)) P

    exp (θ B_t) is integrable.

    source
    theorem ProbabilityTheory.IsPreBrownianReal.integrable_exponentialMartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (θ : ℝ) (t : NNReal) :
    MeasureTheory.Integrable (TauCeti.Probability.exponentialMartingale θ B t) P

    The exponential martingale is integrable at every time.

    source
    theorem ProbabilityTheory.IsPreBrownianReal.integral_exponentialMartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (θ : ℝ) (t : NNReal) :
    ∫ (ω : Ω), TauCeti.Probability.exponentialMartingale θ B t ω ∂P = 1

    The exponential martingale has expectation 1 at every time.

    source
    theorem ProbabilityTheory.IsPreBrownianReal.memLp_exponentialMartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (θ : ℝ) (t : NNReal) {p : ENNReal} (hp : p ≠ ⊤) :
    MeasureTheory.MemLp (TauCeti.Probability.exponentialMartingale θ B t) p P

    The exponential martingale has finite moments of every finite order.

    source
    theorem ProbabilityTheory.IsPreBrownianReal.tilted_mul_eval_eq_withDensity {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (θ : ℝ) (T : NNReal) :
    (P.tilted fun (ω : Ω) => θ * B T ω) = P.withDensity fun (ω : Ω) => ENNReal.ofReal (TauCeti.Probability.exponentialMartingale θ B T ω)

    Tilting P by θ B_T is the change of measure with density exp (θ B_T - θ² T / 2).

    source
    theorem TauCeti.Probability.IsFilteredPreBrownianReal.martingale_exponentialMartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) :
    MeasureTheory.Martingale (exponentialMartingale θ W) ℱ P

    The exponential martingale exp (θ W_t - θ² t / 2) of a Brownian motion relative to ℱ is a martingale relative to ℱ.

    source
    theorem TauCeti.Probability.IsFilteredPreBrownianReal.tilted_mul_eval_apply {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ} (hW : IsFilteredPreBrownianReal ℱ W P) (θ : ℝ) {t T : NNReal} (htT : t ≤ T) {A : Set Ω} (hA : MeasurableSet A) :
    (P.tilted fun (ω : Ω) => θ * W T ω) A = ENNReal.ofReal (∫ (ω : Ω) in A, exponentialMartingale θ W t ω ∂P)

    On an event A known at time t ≤ T, the tilt of P by θ W_T has density Z_t: Q(A) = E[Z_t; A].