PL1/DaugavetIntrinsicFramework.lean

All source files · Download exact source

SHA-256: f8ad515f4066eea0de80b3adf5fdfa2c570b195dacf61f13d96d0ff2118dda5e

1import PL1.DaugavetAveraging2import PL1.IntrinsicWalshBlocks34/-! # The actual dense increasing finite-coordinate intrinsic ranges -/56noncomputable section7open Filter MeasureTheory8open scoped NNReal Topology910namespace PL1.Noise1112variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1314theorem intrinsicExpectation_range_monotone :15    Monotone (fun n => (intrinsicExpectation K rates n).range) := by16  intro m n hmn x hx17  obtain ⟨y, rfl⟩ := hx18  refine ⟨intrinsicExpectation K rates m y, ?_⟩19  change ((intrinsicExpectation K rates n).comp (intrinsicExpectation K rates m)) y = _20  rw [intrinsicExpectation_comp_min, min_eq_right hmn]21  rfl2223theorem dense_iUnion_intrinsicExpectation_range :24    Dense (⋃ n, ((intrinsicExpectation K rates n).range : Set (dyadicSystem K rates).IntrinsicSpace)) := by25  intro x26  apply isClosed_closure.mem_of_tendsto (tendsto_intrinsicExpectation K rates x)27  exact Eventually.of_forall (fun n => subset_closure (Set.mem_iUnion.mpr ⟨n, ⟨x, rfl⟩⟩))2829theorem intrinsicSpace_nontrivial : Nontrivial (dyadicSystem K rates).IntrinsicSpace :=30  ⟨⟨intrinsicCharacter K rates ∅, 0, (linearIndependent_intrinsicCharacter K rates).ne_zero ∅⟩⟩3132theorem intrinsic_sliceCriterion_of_finiteSpikeFamilies33    (hspikes : Daugavet.FiniteSpikeFamilies K (dyadicSystem K rates).IntrinsicSpace34      (fun n => (intrinsicExpectation K rates n).range)) :35    Daugavet.SliceCriterion K (dyadicSystem K rates).IntrinsicSpace :=36  Daugavet.sliceCriterion_of_finiteSpikeFamilies _37    (intrinsicExpectation_range_monotone K rates)38    (dense_iUnion_intrinsicExpectation_range K rates) hspikes3940theorem intrinsic_hasDaugavetProperty_of_finiteSpikeFamilies41    (hspikes : Daugavet.FiniteSpikeFamilies K (dyadicSystem K rates).IntrinsicSpace42      (fun n => (intrinsicExpectation K rates n).range)) :43    Daugavet.HasDaugavetProperty K (dyadicSystem K rates).IntrinsicSpace := by44  let := intrinsicSpace_nontrivial K rates45  exact (intrinsic_sliceCriterion_of_finiteSpikeFamilies K rates hspikes).hasDaugavetProperty4647end PL1.Noise48