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

PL1/ExplicitMartingale.lean

All source files · Download exact source

SHA-256: 4ad23de486bdb255caa91fa1989d2cd22ad8f209dd770a20a4d2132d512a9021

1import PL1.IntrinsicNonBoundedComplete2import PL1.ScalarRealification3import Mathlib.Algebra.BigOperators.Ring.Finset45/-!6# The explicit cylinder-resolvent sequence78The normalized finite cylinder indicators are defined through their finite9Walsh expansions and are identified with the exact indicator functions.10Applying the zeroth reconstruction column gives the manuscript's concrete11bounded coherent sequence in the actual intrinsic Banach space.12-/1314noncomputable section15open MeasureTheory Filter16open scoped ENNReal NNReal Topology BigOperators1718namespace PL1.ExplicitMartingale1920open Walsh WalshExpectations Noise IntrinsicGraph ScalarRealification2122/-- The cylinder through `s` determined by the first `m` coordinates. -/23def cylinder (m : ℕ) (s : Walsh.Group) : Set Walsh.Group :=24  {x | ∀ j : ℕ, j < m → x j = s j}2526/-- The real normalized cylinder kernel, as an actual continuous polynomial. -/27def kernelContinuous (m : ℕ) (s : Walsh.Group) : C(Walsh.Group, ℝ) :=28  ∑ F ∈ (Finset.range m).powerset, character F s • characterContinuous F2930theorem kernelContinuous_apply (m : ℕ) (s x : Walsh.Group) :31    kernelContinuous m s x = ∑ F ∈ (Finset.range m).powerset, character F (s * x) := by32  simp only [kernelContinuous, ContinuousMap.sum_apply, ContinuousMap.smul_apply,33    smul_eq_mul, characterContinuous, ContinuousMap.coe_mk, character_mul]3435theorem kernelContinuous_eq_prod (m : ℕ) (s x : Walsh.Group) :36    kernelContinuous m s x = ∏ j ∈ Finset.range m, (1 + signValue (s j * x j)) := by37  rw [kernelContinuous_apply, Finset.prod_one_add]38  rfl3940theorem one_add_sign_mul (a b : Sign) :41    (1 + signValue (a * b) : ℝ) = if b = a then 2 else 0 := by42  classical43  rw [signValue_mul]44  rcases signValue_eq_one_or_neg_one a with ha | ha <;>45    rcases signValue_eq_one_or_neg_one b with hb | hb46  · have hab : b = a := signValue_injective (hb.trans ha.symm)47    norm_num [ha, hab]48  · have hab : b ≠ a := by intro h; subst b; linarith49    norm_num [ha, hb, hab]50  · have hab : b ≠ a := by intro h; subst b; linarith51    norm_num [ha, hb, hab]52  · have hab : b = a := signValue_injective (hb.trans ha.symm)53    norm_num [ha, hab]5455/-- The finite Walsh polynomial is exactly `2^m` on its cylinder and zero56off that cylinder, at every point rather than only almost everywhere. -/57theorem kernelContinuous_eq_indicator (m : ℕ) (s x : Walsh.Group) :58    kernelContinuous m s x = (cylinder m s).indicator (fun _ => (2 : ℝ) ^ m) x := by59  classical60  rw [kernelContinuous_eq_prod]61  simp_rw [one_add_sign_mul]62  by_cases hx : x ∈ cylinder m s63  · rw [Set.indicator_of_mem hx]64    have h : ∀ j ∈ Finset.range m, x j = s j := fun j hj => hx j (Finset.mem_range.mp hj)65    simp only [Finset.prod_congr rfl (fun j hj => ite_eq_left (h j hj)), Finset.prod_const,66      Finset.card_range]67  · rw [Set.indicator_of_notMem hx]68    have h : ∃ j ∈ Finset.range m, x j ≠ s j := by69      simpa only [cylinder, Set.mem_ofPred_eq, not_forall, exists_prop, Finset.mem_range] using hx70    obtain ⟨j, hj, hneq⟩ := h71    exact Finset.prod_eq_zero hj (ite_eq_right hneq)7273theorem kernelContinuous_nonneg (m : ℕ) (s x : Walsh.Group) :74    0 ≤ kernelContinuous m s x := by75  rw [kernelContinuous_eq_indicator]76  exact Set.indicator_nonneg (fun _ _ => by positivity) _7778theorem integral_kernelContinuous (m : ℕ) (s : Walsh.Group) :79    ∫ x, kernelContinuous m s x ∂haar = 1 := by80  simp only [kernelContinuous, ContinuousMap.sum_apply, ContinuousMap.smul_apply,81    characterContinuous, ContinuousMap.coe_mk, smul_eq_mul]82  rw [integral_finsetSum _ (fun F _ => (integrable_character F).const_mul _)]83  simp_rw [integral_const_mul, Walsh.integral_character]84  simp8586/-- The actual real `L1` normalized cylinder class. -/87def kernelRealL1 (m : ℕ) (s : Walsh.Group) : Lp ℝ 1 haar :=88  ContinuousMap.toLp 1 haar ℝ (kernelContinuous m s)8990theorem kernelRealL1_eq_sum (m : ℕ) (s : Walsh.Group) :91    kernelRealL1 m s = ∑ F ∈ (Finset.range m).powerset, character F s • characterLp 1 F := by92  simp only [kernelRealL1, kernelContinuous, map_sum, map_smul, toLp_characterContinuous]9394theorem coeFn_kernelRealL1 (m : ℕ) (s : Walsh.Group) :95    kernelRealL1 m s =ᵐ[haar] kernelContinuous m s :=96  ContinuousMap.coeFn_toLp haar (kernelContinuous m s)9798theorem norm_kernelRealL1 (m : ℕ) (s : Walsh.Group) : ‖kernelRealL1 m s‖ = 1 := by99  rw [L1.norm_eq_integral_norm]100  calc101    _ = ∫ x, kernelContinuous m s x ∂haar := by102      apply integral_congr_ae103      filter_upwards [coeFn_kernelRealL1 m s] with x hx104      rw [hx, Real.norm_of_nonneg (kernelContinuous_nonneg m s x)]105    _ = 1 := integral_kernelContinuous m s106107variable (K : Type*) [RCLike K]108109/-- Scalar-valued normalized cylinder class, with the same real indicator. -/110def kernelL1 (m : ℕ) (s : Walsh.Group) : Lp K 1 haar := ofRealL1 K (kernelRealL1 m s)111112theorem kernelL1_eq_sum (m : ℕ) (s : Walsh.Group) :113    kernelL1 K m s = ∑ F ∈ (Finset.range m).powerset,114      (character F s : K) • scalarCharacterLp K 1 F := by115  rw [kernelL1, kernelRealL1_eq_sum]116  simp only [map_sum, map_smul, ofRealL1_character]117  apply Finset.sum_congr rfl118  intro F hF119  exact (IsScalarTower.algebraMap_smul K (character F s) (scalarCharacterLp K 1 F)).symm120121theorem coeFn_kernelL1 (m : ℕ) (s : Walsh.Group) :122    kernelL1 K m s =ᵐ[haar] fun x => ((kernelContinuous m s x : ℝ) : K) :=123  (coeFn_ofRealL1 K (kernelRealL1 m s)).trans ((coeFn_kernelRealL1 m s).fun_comp _)124125theorem norm_kernelL1 (m : ℕ) (s : Walsh.Group) : ‖kernelL1 K m s‖ = 1 := by126  rw [L1.norm_eq_integral_norm]127  calc128    _ = ∫ x, kernelContinuous m s x ∂haar := by129      apply integral_congr_ae130      filter_upwards [coeFn_kernelL1 K m s] with x hx131      rw [hx, RCLike.norm_ofReal, abs_of_nonneg (kernelContinuous_nonneg m s x)]132    _ = 1 := integral_kernelContinuous m s133134theorem expectation_kernelL1 (k m : ℕ) (s : Walsh.Group) :135    expectationL1 K k (kernelL1 K m s) = kernelL1 K (min k m) s := by136  classical137  have hfilter : ((Finset.range m).powerset.filter (fun F => F ⊆ Finset.range k)) =138      (Finset.range (min k m)).powerset := by139    ext F140    simp only [Finset.mem_filter, Finset.mem_powerset, Finset.subset_iff, Finset.mem_range]141    constructor142    · rintro ⟨hm, hk⟩ j hj143      exact lt_min (hk hj) (hm hj)144    · intro h145      exact ⟨fun j hj => (lt_min_iff.mp (h hj)).2, fun j hj => (lt_min_iff.mp (h hj)).1⟩146  rw [kernelL1_eq_sum, map_sum]147  simp_rw [map_smul, expectationL1_character, smul_ite, smul_zero]148  rw [← Finset.sum_filter, hfilter, kernelL1_eq_sum]149150/-- Walsh moments of the actual normalized cylinder class. -/151theorem fourier_kernelRealL1 (F : Finset ℕ) (m : ℕ) (s : Walsh.Group) :152    SingularConvolution.fourierFunctional F (kernelRealL1 m s) =153      if F ⊆ Finset.range m then character F s else 0 := by154  classical155  rw [kernelRealL1_eq_sum, map_sum]156  simp_rw [map_smul, smul_eq_mul, SingularConvolution.fourierFunctional_character]157  simp [Finset.mem_powerset, mul_ite]158159/-- The actual intrinsic-space-valued cylinder-resolvent functions. -/160def beta (rates : ℕ → ℝ≥0) (m : ℕ) (s : Walsh.Group) :161    (dyadicSystem K rates).IntrinsicSpace :=162  (dyadicSystem K rates).column 0 (kernelL1 K m s)163164/-- The fixed sequence from the manuscript is the trajectory through the165group identity: `R₁(2^m 1_{H_m})`. -/166def sequence (rates : ℕ → ℝ≥0) (m : ℕ) : (dyadicSystem K rates).IntrinsicSpace :=167  beta K rates m 1168169theorem evalZero_beta (rates : ℕ → ℝ≥0) (m : ℕ) (s : Walsh.Group) :170    evalZero (dyadicSystem K rates).analysis (beta K rates m s) =171      resolventL1 K rates (dyadicTime 0) (kernelL1 K m s) := by172  rw [beta, DyadicSystem.evalZero_column]173  rfl174175theorem norm_beta_le (rates : ℕ → ℝ≥0) (m : ℕ) (s : Walsh.Group) :176    ‖beta K rates m s‖ ≤ projectionBound := by177  have h := ((dyadicSystem K rates).column 0).le_opNorm (kernelL1 K m s)178  rw [norm_kernelL1, mul_one] at h179  exact h.trans ((dyadicSystem K rates).norm_column_le 0)180181theorem norm_sequence_le (rates : ℕ → ℝ≥0) (m : ℕ) :182    ‖sequence K rates m‖ ≤ projectionBound := norm_beta_le K rates m 1183184/-- Coherence holds for all two indices, with the exact minimum formula. -/185theorem intrinsicExpectation_beta (rates : ℕ → ℝ≥0) (k m : ℕ) (s : Walsh.Group) :186    intrinsicExpectation K rates k (beta K rates m s) = beta K rates (min k m) s := by187  apply evalZero_injective (dyadicSystem K rates).analysis188  rw [evalZero_intrinsicExpectation, evalZero_beta, evalZero_beta]189  have h := DFunLike.congr_fun190    (expectationL1_resolvent_commute K k rates (dyadicTime 0)) (kernelL1 K m s)191  change expectationL1 K k (resolventL1 K rates (dyadicTime 0) (kernelL1 K m s)) =192    resolventL1 K rates (dyadicTime 0) (expectationL1 K k (kernelL1 K m s)) at h193  rw [h, expectation_kernelL1]194195theorem intrinsicExpectation_sequence (rates : ℕ → ℝ≥0) (k m : ℕ) :196    intrinsicExpectation K rates k (sequence K rates m) = sequence K rates (min k m) :=197  intrinsicExpectation_beta K rates k m 1198199omit K in200/-- Singular convolution of these actual cylinder kernels is not Cauchy201in Haar `L1`, for any cylinder trajectory. -/202theorem not_cauchySeq_convolution_kernelRealL1203    (ν : Measure Walsh.Group) [IsProbabilityMeasure ν]204    (N : Set Walsh.Group) (hmN : haar N = 0) (hνN : ν N ≠ 0)205    (s : Walsh.Group) :206    ¬ CauchySeq (fun m => convolutionL1 (𝕜 := ℝ) ν (kernelRealL1 m s)) := by207  intro hc208  obtain ⟨g, hg⟩ := cauchySeq_tendsto_of_complete hc209  have hMom (F : Finset ℕ) : SingularConvolution.fourierFunctional F g =210      coefficient ν F * character F s := by211    have ht := ((SingularConvolution.fourierFunctional F).continuous.tendsto g).comp hg212    have he : Tendsto (fun m => SingularConvolution.fourierFunctional F213        (convolutionL1 ν (kernelRealL1 m s))) atTop214          (𝓝 (coefficient ν F * character F s)) := by215      apply tendsto_const_nhds.congr'216      filter_upwards [eventually_ge_atTop (F.sup id + 1)] with m hm217      have hF : F ⊆ Finset.range m := by218        intro j hj219        exact Finset.mem_range.mpr ((Finset.le_sup (f := id) hj).trans_lt (by omega))220      rw [SingularConvolution.fourierFunctional_convolution_apply, fourier_kernelRealL1,221        ite_eq_left hF]222    exact tendsto_nhds_unique ht he223  let g' := convolutionL1 (𝕜 := ℝ) (Measure.dirac s) g224  apply SingularConvolution.no_integrable_density_of_null_carrier ν N hmN hνN225  refine ⟨g', L1.integrable_coeFn g', ?_⟩226  intro F227  rw [← SingularConvolution.fourierFunctional_apply]228  change SingularConvolution.fourierFunctional F229    (convolutionL1 (𝕜 := ℝ) (Measure.dirac s) g) = coefficient ν F230  rw [SingularConvolution.fourierFunctional_convolution_apply, hMom]231  have hdir : coefficient (Measure.dirac s) F = character F s := by232    simp [coefficient]233  rw [hdir]234  calc235    character F s * (coefficient ν F * character F s) =236        coefficient ν F * (character F s * character F s) := by ring237    _ = coefficient ν F := by rw [character_mul_self, mul_one]238239theorem re_evalZero_beta (rates : ℕ → ℝ≥0) (m : ℕ) (s : Walsh.Group) :240    reL1 K (evalZero (dyadicSystem K rates).analysis (beta K rates m s)) =241      resolventL1 ℝ rates (dyadicTime 0) (kernelRealL1 m s) := by242  let := isProbabilityMeasure_resolventMeasure rates (dyadicTime 0).property243  rw [evalZero_beta]244  exact DFunLike.congr_fun (reL1_convolution_ofRealL1 K245    (resolventMeasure rates (dyadicTime 0))) (kernelRealL1 m s)246247/-- Every trajectory of the explicitly defined intrinsic-space function248fails to be norm Cauchy whenever the actual zeroth resolvent is singular. -/249theorem not_cauchySeq_beta_of_null_carrier (rates : ℕ → ℝ≥0)250    (N : Set Walsh.Group) (hmN : haar N = 0)251    (hνN : resolventMeasure rates (dyadicTime 0) N ≠ 0) (s : Walsh.Group) :252    ¬ CauchySeq (fun m => beta K rates m s) := by253  let := isProbabilityMeasure_resolventMeasure rates (dyadicTime 0).property254  intro hc255  obtain ⟨a, ha⟩ := cauchySeq_tendsto_of_complete hc256  have hzero := ((evalZero (dyadicSystem K rates).analysis).continuous.tendsto a).comp ha257  have hre := ((reL1 K).continuous.tendsto _).comp hzero258  have ht : Tendsto (fun m => convolutionL1 (𝕜 := ℝ)259      (resolventMeasure rates (dyadicTime 0)) (kernelRealL1 m s)) atTop260      (𝓝 (reL1 K (evalZero (dyadicSystem K rates).analysis a))) := by261    convert hre using 1262    funext m263    exact (re_evalZero_beta K rates m s).symm264  exact not_cauchySeq_convolution_kernelRealL1 (resolventMeasure rates (dyadicTime 0))265    N hmN hνN s ht.cauchySeq266267theorem schur_beta_not_cauchy (s : Walsh.Group) :268    ¬ CauchySeq (fun m => beta K schurRates m s) :=269  not_cauchySeq_beta_of_null_carrier K schurRates (Carrier.commonSet 0)270    (Carrier.haar_commonSet_eq_zero 0) (by rw [schur_resolvent_commonSet]; exact one_ne_zero) s271272theorem constant_beta_not_cauchy (s : Walsh.Group) :273    ¬ CauchySeq (fun m => beta K constantRates m s) :=274  not_cauchySeq_beta_of_null_carrier K constantRates (Carrier.commonSet 0)275    (Carrier.haar_commonSet_eq_zero 0) (by rw [constant_resolvent_commonSet]; exact one_ne_zero) s276277theorem schur_sequence_not_cauchy : ¬ CauchySeq (sequence K schurRates) :=278  schur_beta_not_cauchy K 1279280theorem constant_sequence_not_cauchy : ¬ CauchySeq (sequence K constantRates) :=281  constant_beta_not_cauchy K 1282283end PL1.ExplicitMartingale284