Samplinglib
Lean gate passed 2026-08-19T05:09:39.794721+00:00 · 644be936998e
Chapter 3 · Book pp. 96–120 · August 9, 2026 edition

Additional Topics in Stochastic Analysis

Build the stochastic-analysis tools used later for path-space comparison, conditioned diffusions, and bridge constructions.

Begin with 3.1 Open this chapter in the canonical August 9 source ↗

Chapter route

This chapter develops quadratic variation, change of measure, Girsanov theorem, Doob transform. Its main destination is to connect the definitions below to the results that later chapters consume.

Core definitions

  • Quadratic variation records the second-order accumulation of path increments.
  • The stochastic exponential is the path likelihood used for drift changes.
  • A Doob transform conditions or tilts a Markov evolution through a positive space-time function.
  • Föllmer drift and the Schrödinger bridge formulate entropy-minimizing path-space transports.

Main results

  • Brownian quadratic variation produces the correction in Itô calculus.
  • Girsanov's theorem identifies the law of a process after an adapted drift change.
  • Doob's transform gives a conditioned generator and semigroup.
  • Föllmer and Schrödinger constructions connect relative entropy, optimal drift control, and endpoint constraints.

Contents

  1. 3.1Quadratic VariationBook p. 96
  2. 3.2Change of Measure in Path SpaceBook p. 100
  3. 3.3Doob's TransformBook p. 104
  4. 3.4Föllmer DriftBook p. 108
  5. 3.5Schrödinger BridgeBook p. 110
  6. 3.bibBibliographical NotesBook p. 114
  7. 3.exExercisesBook p. 116
Why is this chapter route valid?

Analytic contracts

  • Quadratic-variation limits require an explicit convergence mode and partition scheme.
  • A stochastic exponential needs measurability and integrability conditions before it defines a change of law.
  • Finite-dimensional cylinder identities are not automatically path-space Girsanov theorems.

Open boundaries

  • Full path-space Girsanov package
  • General transportation-entropy equivalences
View Lean formalization

These mappings are evidence links, not a claim that the entire chapter is formalized.