PL1/IntrinsicHeadRepresentatives.lean

All source files · Download exact source

SHA-256: 7554bf8f867a0fa277418af57d5b48912c6f30ae7ffd308ce6de6e38d9375411

1import PL1.IntrinsicWalsh2import PL1.HeadTail34/-!5# Continuous head representatives of intrinsic finite-coordinate vectors67Every coordinate of a vector in the actual intrinsic expectation range has a8continuous representative depending only on the prescribed initial segment.9The equalities below are identities in the original Haar L¹ quotient.10-/1112noncomputable section13open MeasureTheory14open scoped ENNReal NNReal1516namespace PL1.IntrinsicHeadRepresentatives17open Walsh WalshExpectations IntrinsicGraph Noise1819variable {K : Type*} [RCLike K]2021theorem scalarCharacter_dependsOn (m : ℕ) (F : Finset ℕ) (hF : F ⊆ Finset.range m) :22    HeadTail.DependsOn (Finset.range m) (scalarCharacterContinuous K F) := by23  intro x y hxy24  change (character F x : K) = (character F y : K)25  congr 126  unfold character27  apply Finset.prod_congr rfl28  intro j hj29  exact congrArg signValue (hxy j (hF hj))3031theorem continuousRepresentative_of_mem_finiteSpan (m : ℕ) {f : Lp K 1 haar}32    (hf : f ∈ finiteSpan K m) :33    ∃ g : C(Walsh.Group, K), HeadTail.DependsOn (Finset.range m) g ∧34      ContinuousMap.toLp 1 haar K g = f := by35  let H : Submodule K (Lp K 1 haar) := {36    carrier := {f | ∃ g : C(Walsh.Group, K), HeadTail.DependsOn (Finset.range m) g ∧37      ContinuousMap.toLp 1 haar K g = f}38    zero_mem' := ⟨0, (fun _ _ _ => rfl), map_zero _⟩39    add_mem' := by40      rintro _ _ ⟨g, hg, rfl⟩ ⟨h, hh, rfl⟩41      refine ⟨g + h, ?_, map_add _ _ _⟩42      intro x y hxy43      simp only [ContinuousMap.add_apply, hg x y hxy, hh x y hxy]44    smul_mem' := by45      rintro c _ ⟨g, hg, rfl⟩46      refine ⟨c • g, ?_, map_smul _ _ _⟩47      intro x y hxy48      simp only [ContinuousMap.smul_apply, hg x y hxy]49  }50  have hle : finiteSpan K m ≤ H := by51    apply Submodule.span_le.mpr52    rintro _ ⟨F, hF, rfl⟩53    exact ⟨scalarCharacterContinuous K F,54      scalarCharacter_dependsOn m F (Finset.mem_powerset.mp hF),55      toLp_scalarCharacterContinuous K 1 F⟩56  exact hle hf5758theorem analysis_mem_finiteSpan (rates : ℕ → ℝ≥0) (m n : ℕ)59    {f : Lp K 1 haar} (hf : f ∈ finiteSpan K m) :60    (dyadicSystem K rates).analysis n f ∈ finiteSpan K m := by61  have hle : finiteSpan K m ≤ (finiteSpan K m).comap62      ((dyadicSystem K rates).analysis n).toLinearMap := by63    apply Submodule.span_le.mpr64    rintro _ ⟨F, hF, rfl⟩65    have hmem := character_mem_finiteSpan K m F (Finset.mem_powerset.mp hF)66    change (dyadicSystem K rates).analysis n (scalarCharacterLp K 1 F) ∈ finiteSpan K m67    cases n with68    | zero => exact hmem69    | succ n =>70      change (((ResolventEstimates.dyadicRatio ^ (n + 1))⁻¹ : ℝ) : K) •71          (scalarCharacterLp K 1 F - resolventL1 K rates (dyadicTime (n + 1))72            (scalarCharacterLp K 1 F)) ∈ finiteSpan K m73      rw [resolventL1_scalarCharacter]74      exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hmem (Submodule.smul_mem _ _ hmem))75  exact hle hf7677theorem coord_mem_finiteSpan_of_range (rates : ℕ → ℝ≥0) (m n : ℕ)78    {f : (dyadicSystem K rates).IntrinsicSpace}79    (hf : f ∈ (intrinsicExpectation K rates m).range) :80    coord (dyadicSystem K rates).analysis n f ∈ finiteSpan K m := by81  obtain ⟨g, rfl⟩ := hf82  change coord (dyadicSystem K rates).analysis n (intrinsicExpectation K rates m g) ∈83    finiteSpan K m84  rw [coord_intrinsicExpectation]85  exact expectationL1_mem_finiteSpan K m _8687theorem continuousRepresentative_coord_of_range (rates : ℕ → ℝ≥0) (m n : ℕ)88    {f : (dyadicSystem K rates).IntrinsicSpace}89    (hf : f ∈ (intrinsicExpectation K rates m).range) :90    ∃ g : C(Walsh.Group, K), HeadTail.DependsOn (Finset.range m) g ∧91      ContinuousMap.toLp 1 haar K g = coord (dyadicSystem K rates).analysis n f :=92  continuousRepresentative_of_mem_finiteSpan m (coord_mem_finiteSpan_of_range rates m n hf)9394theorem continuousRepresentative_evalZero_of_range (rates : ℕ → ℝ≥0) (m : ℕ)95    {f : (dyadicSystem K rates).IntrinsicSpace}96    (hf : f ∈ (intrinsicExpectation K rates m).range) :97    ∃ g : C(Walsh.Group, K), HeadTail.DependsOn (Finset.range m) g ∧98      ContinuousMap.toLp 1 haar K g = evalZero (dyadicSystem K rates).analysis f :=99  continuousRepresentative_coord_of_range rates m 0 hf100101end PL1.IntrinsicHeadRepresentatives102