On complemented subspaces of L1[0,1]L_1[0,1]

PL1/ExplicitMartingaleFiltration.lean

All source files · Download exact source

SHA-256: 58d0c4ae0c2d555d7bb5bca30e48ae1378abcbcf464e24833ac0c1f231909760

1import PL1.ExplicitMartingale2import Mathlib.Probability.Martingale.Basic34/-!5# The actual first-coordinate filtration and its Walsh conditional expectations67The filtration is the pullback of the measurable space on the first `m`8sign coordinates. Its conditional expectation is computed by invariance9under flipping any unseen coordinate.10-/1112noncomputable section13open MeasureTheory Filter14open scoped ENNReal NNReal Topology BigOperators ProbabilityTheory1516namespace PL1.ExplicitMartingale17open Walsh WalshExpectations Noise IntrinsicGraph ScalarRealification1819def prefixMap (m : ℕ) (s : Walsh.Group) : Fin m → Sign := fun j => s j2021def extendPrefix (m : ℕ) (w : Fin m → Sign) : Walsh.Group :=22  fun j => if h : j < m then w ⟨j, h⟩ else 12324/-- The sigma-algebra generated by precisely the first `m` coordinates. -/25@[instance_reducible] def coordinateSpace (m : ℕ) : MeasurableSpace Walsh.Group :=26  MeasurableSpace.comap (prefixMap m) inferInstance2728theorem coordinateSpace_mono : Monotone coordinateSpace := by29  intro m n hmn30  exact MeasurableSpace.comap_le_comap_of_eq_comp31    (fun w : Fin n → Sign => fun j : Fin m => w ⟨j, j.isLt.trans_le hmn⟩)32    (measurable_of_finite _) rfl3334theorem coordinateSpace_le (m : ℕ) : coordinateSpace m ≤ (inferInstance : MeasurableSpace Walsh.Group) :=35  (show Measurable (prefixMap m) from36    Measurable.of_eval (fun j => measurable_pi_apply (j : ℕ))).comap_le3738def coordinateFiltration : Filtration ℕ (inferInstance : MeasurableSpace Walsh.Group) where39  seq := coordinateSpace40  mono' := coordinateSpace_mono41  le' := coordinateSpace_le4243theorem character_extendPrefix {F : Finset ℕ} {m : ℕ} (hF : F ⊆ Finset.range m)44    (s : Walsh.Group) : character F (extendPrefix m (prefixMap m s)) = character F s := by45  unfold character46  apply Finset.prod_congr rfl47  intro j hj48  simp only [extendPrefix, Finset.mem_range.mp (hF hj), dite_true, prefixMap]4950theorem stronglyMeasurable_character_coordinateSpace {F : Finset ℕ} {m : ℕ}51    (hF : F ⊆ Finset.range m) : StronglyMeasurable[coordinateSpace m] (character F) := by52  have h : Measurable[coordinateSpace m]53      (fun s => character F (extendPrefix m (prefixMap m s))) :=54    (measurable_of_finite (fun w : Fin m → Sign => character F (extendPrefix m w))).comp55      (comap_measurable (prefixMap m))56  simpa only [character_extendPrefix hF] using h.stronglyMeasurable5758theorem prefix_flip_mul (m j : ℕ) (hj : m ≤ j) (x : Walsh.Group) :59    prefixMap m (flip j * x) = prefixMap m x := by60  funext i61  have hij : (i : ℕ) ≠ j := by omega62  simp only [prefixMap, Pi.mul_apply, Walsh.flip, Function.update_of_ne hij, Pi.one_apply, one_mul]6364/-- An unseen Walsh coordinate forces zero integral over every event in65the first-coordinate sigma-algebra. -/66theorem setIntegral_character_eq_zero_of_not_subset (m : ℕ) (F : Finset ℕ)67    (hF : ¬ F ⊆ Finset.range m) (A : Set Walsh.Group)68    (hA : MeasurableSet[coordinateSpace m] A) : ∫ x in A, character F x ∂haar = 0 := by69  classical70  obtain ⟨j, hjF, hjm⟩ := Finset.not_subset.mp hF71  have hj : m ≤ j := Nat.le_of_not_gt (by simpa only [Finset.mem_range] using hjm)72  rw [← integral_indicator (coordinateSpace_le m A hA)]73  apply integral_eq_zero_of_mul_left_eq_neg (g := flip j)74  intro x75  have hAx : flip j * x ∈ A ↔ x ∈ A := by76    obtain ⟨B, _, rfl⟩ := hA77    change prefixMap m (flip j * x) ∈ B ↔ prefixMap m x ∈ B78    rw [prefix_flip_mul m j hj]79  by_cases hx : x ∈ A80  · rw [Set.indicator_of_mem (hAx.mpr hx), Set.indicator_of_mem hx,81      character_mul, character_flip_of_mem hjF, neg_one_mul]82  · rw [Set.indicator_of_notMem (fun h => hx (hAx.mp h)), Set.indicator_of_notMem hx, neg_zero]8384/-- Conditional expectation in the genuine coordinate filtration acts on85Walsh characters by deleting exactly the unseen characters. -/86theorem condExp_character (m : ℕ) (F : Finset ℕ) :87    haar[character F | coordinateSpace m] =ᵐ[haar]88      fun x => if F ⊆ Finset.range m then character F x else 0 := by89  classical90  by_cases hF : F ⊆ Finset.range m91  · simp only [hF, ite_true]92    rw [condExp_of_stronglyMeasurable (coordinateSpace_le m)93      (stronglyMeasurable_character_coordinateSpace hF) (integrable_character F)]94  · simp only [hF, ite_false]95    apply Filter.EventuallyEq.symm96    apply ae_eq_condExp_of_forall_setIntegral_eq (coordinateSpace_le m) (integrable_character F)97    · intro A hA hμA98      exact (integrable_zero _ _ _).integrableOn99    · intro A hA hμA100      rw [integral_zero, setIntegral_character_eq_zero_of_not_subset m F hF A hA]101    · exact stronglyMeasurable_const.aestronglyMeasurable102103section VectorWalsh104105variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]106107/-- Finite Walsh expansions with fixed Banach-space-valued coefficients. -/108def walshProcess (v : Finset ℕ → E) (m : ℕ) : Walsh.Group → E :=109  ∑ F ∈ (Finset.range m).powerset, fun s => character F s • v F110111theorem integrable_walshProcess (v : Finset ℕ → E) (m : ℕ) :112    Integrable (walshProcess v m) haar := by113  apply integrable_finsetSum' _114  intro F hF115  exact (integrable_character F).smul_const (v F)116117theorem stronglyAdapted_walshProcess (v : Finset ℕ → E) :118    StronglyAdapted coordinateFiltration (walshProcess v) := by119  intro m120  unfold walshProcess121  apply Finset.stronglyMeasurable_sum122  intro F hF123  exact (stronglyMeasurable_character_coordinateSpace (Finset.mem_powerset.mp hF)).smul124    stronglyMeasurable_const125126variable [CompleteSpace E]127128theorem condExp_character_smul (m : ℕ) (F : Finset ℕ) (v : E) :129    haar[(fun s => character F s • v) | coordinateSpace m] =ᵐ[haar]130      fun s => if F ⊆ Finset.range m then character F s • v else 0 := by131  classical132  have h := condExp_smul_of_aestronglyMeasurable_right (m := coordinateSpace m)133    (integrable_character F) ((integrable_character F).smul_const v)134    (stronglyMeasurable_const (b := v)).aestronglyMeasurable135  filter_upwards [h, condExp_character m F] with s hs hc136  change haar[(fun s => character F s • v) | coordinateSpace m] s =137    haar[character F | coordinateSpace m] s • v at hs138  simpa only [hc, ite_smul, zero_smul] using hs139140theorem condExp_walshProcess (v : Finset ℕ → E) (k m : ℕ) :141    haar[walshProcess v m | coordinateSpace k] =ᵐ[haar]142      walshProcess v (min k m) := by143  classical144  have hfilter : ((Finset.range m).powerset.filter (fun F => F ⊆ Finset.range k)) =145      (Finset.range (min k m)).powerset := by146    ext F147    simp only [Finset.mem_filter, Finset.mem_powerset, Finset.subset_iff, Finset.mem_range]148    constructor149    · rintro ⟨hm, hk⟩ j hj150      exact lt_min (hk hj) (hm hj)151    · intro h152      exact ⟨fun j hj => (lt_min_iff.mp (h hj)).2, fun j hj => (lt_min_iff.mp (h hj)).1⟩153  have hsum := condExp_finsetSum (s := (Finset.range m).powerset)154    (f := fun F s => character F s • v F)155    (fun F _ => (integrable_character F).smul_const (v F)) (coordinateSpace k)156  have hall : ∀ᵐ s ∂haar, ∀ F,157      haar[(fun t => character F t • v F) | coordinateSpace k] s =158        if F ⊆ Finset.range k then character F s • v F else 0 := by159    exact ae_all_iff.mpr fun F => condExp_character_smul k F (v F)160  filter_upwards [hsum, hall] with s hs ha161  change haar[walshProcess v m | coordinateSpace k] s = _ at hs ⊢162  rw [hs]163  simp only [Finset.sum_apply]164  simp_rw [ha]165  rw [← Finset.sum_filter, hfilter]166  simp only [walshProcess, Finset.sum_apply]167168theorem martingale_walshProcess (v : Finset ℕ → E) :169    Martingale (walshProcess v) coordinateFiltration haar := by170  refine ⟨stronglyAdapted_walshProcess v, ?_⟩171  intro k m hkm172  simpa only [coordinateFiltration, min_eq_left hkm] using condExp_walshProcess v k m173174end VectorWalsh175176variable (K : Type*) [RCLike K]177178local instance betaRealNormedSpace (rates : ℕ → ℝ≥0) :179    NormedSpace ℝ (dyadicSystem K rates).IntrinsicSpace :=180  NormedSpace.restrictScalars ℝ K (dyadicSystem K rates).IntrinsicSpace181182theorem beta_eq_walshProcess (rates : ℕ → ℝ≥0) :183    beta K rates = walshProcess (fun F =>184      ((dyadicSystem K rates).column 0 (scalarCharacterLp K 1 F) :185        (dyadicSystem K rates).IntrinsicSpace)) := by186  let := IsScalarTower.restrictScalars ℝ K (dyadicSystem K rates).IntrinsicSpace187  funext m s188  simp only [beta, kernelL1_eq_sum, map_sum, map_smul, walshProcess, Finset.sum_apply]189  rfl190191/-- The manuscript's explicit process is a genuine Mathlib martingale192for the first-coordinate filtration, over both real and complex scalars. -/193theorem martingale_beta (rates : ℕ → ℝ≥0) :194    letI := NormedSpace.restrictScalars ℝ K (dyadicSystem K rates).IntrinsicSpace195    Martingale (beta K rates) coordinateFiltration haar := by196  let := NormedSpace.restrictScalars ℝ K (dyadicSystem K rates).IntrinsicSpace197  rw [beta_eq_walshProcess]198  exact martingale_walshProcess _199200theorem schur_explicit_martingale :201    letI := NormedSpace.restrictScalars ℝ K (dyadicSystem K schurRates).IntrinsicSpace202    Martingale (beta K schurRates) coordinateFiltration haar ∧203      (∀ m s, ‖beta K schurRates m s‖ ≤ projectionBound) ∧204      (∀ s, ¬ CauchySeq (fun m => beta K schurRates m s)) :=205  ⟨martingale_beta K schurRates, norm_beta_le K schurRates, schur_beta_not_cauchy K⟩206207theorem constant_explicit_martingale :208    letI := NormedSpace.restrictScalars ℝ K (dyadicSystem K constantRates).IntrinsicSpace209    Martingale (beta K constantRates) coordinateFiltration haar ∧210      (∀ m s, ‖beta K constantRates m s‖ ≤ projectionBound) ∧211      (∀ s, ¬ CauchySeq (fun m => beta K constantRates m s)) :=212  ⟨martingale_beta K constantRates, norm_beta_le K constantRates, constant_beta_not_cauchy K⟩213214end PL1.ExplicitMartingale215