Martingale transforms and the Lp Burkholder inequality

Defines the discrete martingale transform and proves the sharp Lp Burkholder inequality for martingale transforms by a predictable multiplier bounded by 1.

noncomputable def Burkholder.q (p : ℝ) : ℝ

The conjugate exponent helper, re-exported in the Burkholder namespace.

Equations

• Burkholder.q p = Majorants.q p

noncomputable def Burkholder.pStar (p : ℝ) : ℝ

pStar = max p q, re-exported in the Burkholder namespace.

Equations

• Burkholder.pStar p = Majorants.pStar p

noncomputable def Burkholder.v (p x y : ℝ) : ℝ

The Burkholder function v, imported from the majorant development.

Equations

• Burkholder.v p x y = Majorants.v p x y

def MeasureTheory.martingaleDiff {Ω : Type u_1} (f : ℕ → Ω → ℝ) : ℕ → Ω → ℝ

The martingale difference sequence associated to a discrete real-valued process.

With this convention, martingaleDiff f 0 = f 0 and martingaleDiff f (n + 1) = f (n + 1) - f n.

Equations

• MeasureTheory.martingaleDiff f 0 = f 0
• MeasureTheory.martingaleDiff f n.succ = f (n + 1) - f n

def MeasureTheory.martingaleTransform {Ω : Type u_1} (v f : ℕ → Ω → ℝ) : ℕ → Ω → ℝ

The discrete martingale transform of f by the multiplier process v.

If f has difference sequence d, then the transformed process has difference sequence v n * d n.

Equations

• MeasureTheory.martingaleTransform v f n = ∑ i ∈ Finset.range (n + 1), v i * MeasureTheory.martingaleDiff f i

def MeasureTheory.«term_⋆ₘ_» : Lean.TrailingParserDescr

Notation v ⋆ₘ f for the discrete martingale transform of f by v.

Equations

• MeasureTheory.«term_⋆ₘ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⋆ₘ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ₘ ") (Lean.ParserDescr.cat `term 71))

def MeasureTheory.IsMartingaleTransform {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (ℱ : Filtration ℕ mΩ) (μ : Measure Ω) (v f g : ℕ → Ω → ℝ) : Prop

g is the martingale transform of the martingale f by a strongly predictable multiplier v, relative to the filtration ℱ and measure μ.

Equations

• MeasureTheory.IsMartingaleTransform ℱ μ v f g = (MeasureTheory.IsStronglyPredictable ℱ v ∧ MeasureTheory.Martingale f ℱ μ ∧ g = MeasureTheory.martingaleTransform v f)

theorem MeasureTheory.martingaleTransform_martingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {ℱ : Filtration ℕ mΩ} {v f : ℕ → Ω → ℝ} (hv : IsStronglyPredictable ℱ v) (hf : Martingale f ℱ μ) (hbounded : ∃ (C : ℝ), ∀ (n : ℕ) (ω : Ω), |v n ω| ≤ C) : Martingale (martingaleTransform v f) ℱ μ

A strongly predictable transform of a martingale is a martingale, once the usual integrability and adaptedness hypotheses for the transformed process are available.

The only integrability assumption specific to the multiplier is that each product v (n+1) * (f (n+1) - f n) is integrable; predictability then pulls v (n+1) out of the conditional expectation.

def MeasureTheory.«termX_{_}[_,_]» : Lean.ParserDescr

Notation X_{n}[w,f] for the n-th term of the transform of f by plusOne w.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«termY_{_}[_,_]» : Lean.ParserDescr

Notation Y_{n}[w,f] for the n-th term of the transform of f by minusOne w.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Lp_Burkholder_inequality_martingaleTransform (p : ENNReal) (Ω : Type u_2) [mΩ : MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] (ℱ : Filtration ℕ mΩ) (w f : ℕ → Ω → ℝ) (hp_one : 1 < p) (hfin : p ≠ ⊤) (hstrong : IsStronglyPredictable ℱ w) (hmart : Martingale f ℱ μ) (hLp : ∀ (n : ℕ), MemLp (f n) p μ) (hbound : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, |w n ω| ≤ 1) (n : ℕ) : eLpNorm (martingaleTransform w f n) p μ ≤ ENNReal.ofReal (Burkholder.pStar p.toReal - 1) * eLpNorm (f n) p μ

Burkholder's L^p inequality for discrete martingale transforms.

If f is a martingale and w is a strongly predictable multiplier uniformly bounded by 1, then transforming f by w does not blow up its L^p size by more than the Burkholder factor pStar(p)-1.

The statement is pointwise in time n and is written using eLpNorm: ‖(w ⋆ₘ f)_n‖_p ≤ (pStar(p)-1) * ‖f_n‖_p.