Canonical real iid walks

This file constructs the canonical independent real sequence with values in ℕ → ℝ, its partial and block sums, and proves the fresh-start independence and product-law formulas.

def BGW.Probability.RealWalk.partialSum (ω : ℕ → ℝ) (m : ℕ) : ℝ

The partial sum ω 0 + ⋯ + ω (m-1).

Equations

• BGW.Probability.RealWalk.partialSum ω m = ∑ i ∈ Finset.range m, ω i

def BGW.Probability.RealWalk.blockSum (ω : ℕ → ℝ) (a m : ℕ) : ℝ

The block sum ω a + ⋯ + ω (a+m-1).

Equations

• BGW.Probability.RealWalk.blockSum ω a m = ∑ i ∈ Finset.range m, ω (a + i)

def BGW.Probability.RealWalk.prefixVec (m : ℕ) (ω : ℕ → ℝ) : Fin m → ℝ

The prefix (ω 0, …, ω (m-1)).

Equations

• BGW.Probability.RealWalk.prefixVec m ω i = ω ↑i

def BGW.Probability.RealWalk.shift (k : ℕ) (ω : ℕ → ℝ) : ℕ → ℝ

The shifted sequence i ↦ ω (k + i).

Equations

• BGW.Probability.RealWalk.shift k ω i = ω (k + i)

def BGW.Probability.RealWalk.blockVec (a m : ℕ) (ω : ℕ → ℝ) : Fin m → ℝ

The block (ω a, …, ω (a+m-1)).

Equations

• BGW.Probability.RealWalk.blockVec a m ω i = ω (a + ↑i)

theorem BGW.Probability.RealWalk.partialSum_eq_blockSum (ω : ℕ → ℝ) (m : ℕ) : partialSum ω m = blockSum ω 0 m

theorem BGW.Probability.RealWalk.blockSum_eq_partialSum_shift (ω : ℕ → ℝ) (a m : ℕ) : blockSum ω a m = partialSum (shift a ω) m

theorem BGW.Probability.RealWalk.partialSum_add (ω : ℕ → ℝ) (m k : ℕ) : partialSum ω (m + k) = partialSum ω m + blockSum ω m k

theorem BGW.Probability.RealWalk.measurable_partialSum (m : ℕ) : Measurable fun (ω : ℕ → ℝ) => partialSum ω m

theorem BGW.Probability.RealWalk.measurable_blockSum (a m : ℕ) : Measurable fun (ω : ℕ → ℝ) => blockSum ω a m

theorem BGW.Probability.RealWalk.measurable_prefixVec (m : ℕ) : Measurable (prefixVec m)

theorem BGW.Probability.RealWalk.measurable_shift (k : ℕ) : Measurable (shift k)

theorem BGW.Probability.RealWalk.measurable_blockVec (a m : ℕ) : Measurable (blockVec a m)

noncomputable def BGW.Probability.RealWalk.iidLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) : MeasureTheory.ProbabilityMeasure (ℕ → ℝ)

The canonical real iid law ν ^ ⊗ ℕ on sequences.

Equations

• BGW.Probability.RealWalk.iidLaw ν = ⟨MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑ν, ⋯⟩

theorem BGW.Probability.RealWalk.coe_iidLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) : ↑(iidLaw ν) = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑ν

theorem BGW.Probability.RealWalk.iIndepFun_coord (ν : MeasureTheory.ProbabilityMeasure ℝ) : ProbabilityTheory.iIndepFun (fun (i : ℕ) (ω : ℕ → ℝ) => ω i) ↑(iidLaw ν)

The coordinates are independent under iidLaw ν.

theorem BGW.Probability.RealWalk.map_coord (ν : MeasureTheory.ProbabilityMeasure ℝ) (i : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℝ) => ω i) ↑(iidLaw ν) = ↑ν

Every coordinate has law ν.

theorem BGW.Probability.RealWalk.iidLaw_map_prefix (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) : MeasureTheory.Measure.map (prefixVec m) ↑(iidLaw ν) = MeasureTheory.Measure.pi fun (x : Fin m) => ↑ν

The prefix of length m has the product law.

theorem BGW.Probability.RealWalk.iidLaw_map_block (ν : MeasureTheory.ProbabilityMeasure ℝ) (a m : ℕ) : MeasureTheory.Measure.map (blockVec a m) ↑(iidLaw ν) = MeasureTheory.Measure.pi fun (x : Fin m) => ↑ν

Any block of length m (starting anywhere) has the product law.

theorem BGW.Probability.RealWalk.indepFun_prefix_suffix (ν : MeasureTheory.ProbabilityMeasure ℝ) (m k : ℕ) : ProbabilityTheory.IndepFun (prefixVec m) (blockVec m k) ↑(iidLaw ν)

Two disjoint consecutive blocks are independent.

theorem BGW.Probability.RealWalk.indep_prefix_shift (ν : MeasureTheory.ProbabilityMeasure ℝ) (k : ℕ) : ProbabilityTheory.Indep (MeasurableSpace.comap (prefixVec k) inferInstance) (MeasurableSpace.comap (shift k) inferInstance) ↑(iidLaw ν)

Fresh start: the prefix and shifted-sequence σ-algebras are independent.

theorem BGW.Probability.RealWalk.indepFun_prefix_shift (ν : MeasureTheory.ProbabilityMeasure ℝ) (k : ℕ) : ProbabilityTheory.IndepFun (prefixVec k) (shift k) ↑(iidLaw ν)

Fresh start, function form.

theorem BGW.Probability.RealWalk.iidLaw_map_shift (ν : MeasureTheory.ProbabilityMeasure ℝ) (k : ℕ) : MeasureTheory.Measure.map (shift k) ↑(iidLaw ν) = ↑(iidLaw ν)

The shifted sequence again has law iidLaw ν.

theorem BGW.Probability.RealWalk.measure_prefix_inter_shift (ν : MeasureTheory.ProbabilityMeasure ℝ) (k : ℕ) {A : Set (Fin k → ℝ)} (hA : MeasurableSet A) {C : Set (ℕ → ℝ)} (hC : MeasurableSet C) : ↑(iidLaw ν) (prefixVec k ⁻¹' A ∩ shift k ⁻¹' C) = ↑(iidLaw ν) (prefixVec k ⁻¹' A) * ↑(iidLaw ν) C

Fresh-start product formula for a prefix event A and a future event C.

noncomputable def BGW.Probability.RealWalk.sumLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) : MeasureTheory.ProbabilityMeasure ℝ

The law of the sum of m iid steps.

Equations

• BGW.Probability.RealWalk.sumLaw ν m = (BGW.Probability.RealWalk.iidLaw ν).map fun (ω : ℕ → ℝ) => BGW.Probability.RealWalk.partialSum ω m

theorem BGW.Probability.RealWalk.coe_sumLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) : ↑(sumLaw ν m) = MeasureTheory.Measure.map (fun (ω : ℕ → ℝ) => partialSum ω m) ↑(iidLaw ν)

noncomputable def BGW.Probability.RealWalk.scaledSumLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (B : ℕ → ℝ) (m : ℕ) : MeasureTheory.ProbabilityMeasure ℝ

The law of the sum of m iid steps divided by B m.

Equations

• BGW.Probability.RealWalk.scaledSumLaw ν B m = (BGW.Probability.RealWalk.sumLaw ν m).map fun (x : ℝ) => x / B m

theorem BGW.Probability.RealWalk.iidLaw_map_blockSum (ν : MeasureTheory.ProbabilityMeasure ℝ) (a m : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℝ) => blockSum ω a m) ↑(iidLaw ν) = ↑(sumLaw ν m)

A block sum of length m, started anywhere, has law sumLaw ν m.

theorem BGW.Probability.RealWalk.indepFun_blockSum (ν : MeasureTheory.ProbabilityMeasure ℝ) (m k : ℕ) : ProbabilityTheory.IndepFun (fun (ω : ℕ → ℝ) => blockSum ω 0 m) (fun (ω : ℕ → ℝ) => blockSum ω m k) ↑(iidLaw ν)

Consecutive block sums are independent.

theorem BGW.Probability.RealWalk.iIndepFun_blockSum (ν : MeasureTheory.ProbabilityMeasure ℝ) {k : ℕ} (a m : Fin k → ℕ) (hdisj : ∀ (i j : Fin k), i < j → a i + m i ≤ a j) : ProbabilityTheory.iIndepFun (fun (i : Fin k) (ω : ℕ → ℝ) => blockSum ω (a i) (m i)) ↑(iidLaw ν)

Any finite family of pairwise disjoint blocks gives independent sums.

theorem BGW.Probability.RealWalk.sumLaw_zero (ν : MeasureTheory.ProbabilityMeasure ℝ) : ↑(sumLaw ν 0) = MeasureTheory.Measure.dirac 0

theorem BGW.Probability.RealWalk.sumLaw_succ (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) : ↑(sumLaw ν (m + 1)) = (↑(sumLaw ν m)).conv ↑ν

theorem BGW.Probability.RealWalk.sumLaw_add (ν : MeasureTheory.ProbabilityMeasure ℝ) (m k : ℕ) : ↑(sumLaw ν (m + k)) = (↑(sumLaw ν m)).conv ↑(sumLaw ν k)

theorem BGW.Probability.RealWalk.charFun_sumLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) (u : ℝ) : MeasureTheory.charFun (↑(sumLaw ν m)) u = MeasureTheory.charFun (↑ν) u ^ m

The characteristic function of a sum of m iid steps is charFun ν u ^ m.

theorem BGW.Probability.RealWalk.charFun_scaledSumLaw (ν : MeasureTheory.ProbabilityMeasure ℝ) (B : ℕ → ℝ) (m : ℕ) (u : ℝ) : MeasureTheory.charFun (↑(scaledSumLaw ν B m)) u = MeasureTheory.charFun (↑ν) (u / B m) ^ m

Characteristic function of the scaled sum: charFun ν (u / B m) ^ m.