StepAlgebra.lean

1import BFPP.StepFunctions2import Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization3import Mathlib.Topology.ContinuousMap.StoneWeierstrass45/-! # The algebra generated by initial-segment functions -/67namespace BFPP89set_option autoImplicit false1011open Set Order Filter Topology12open scoped ZeroAtInfty1314universe u15variable {ι : Type u} [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]16  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]1718theorem initialStep_mul (i j : ι) : initialStep i * initialStep j = initialStep (min i j) := by19  ext k20  simp only [ZeroAtInftyContinuousMap.mul_apply, initialStep_apply, le_min_iff]21  split_ifs <;> simp_all2223noncomputable def stepSpan : Submodule ℝ C₀(ι, ℝ) := LinearMap.range stepCombination2425theorem initialStep_mem_stepSpan (i : ι) : initialStep i ∈ (stepSpan : Submodule ℝ C₀(ι, ℝ)) :=26  ⟨Finsupp.single i 1, stepCombination_single i⟩2728theorem stepCombination_eq_sum (c : ι →₀ ℝ) :29    stepCombination c = ∑ i ∈ c.support, c i • initialStep i := rfl3031theorem stepSpan_mul_mem (f g : C₀(ι, ℝ)) (hf : f ∈ stepSpan) (hg : g ∈ stepSpan) :32    f * g ∈ stepSpan := by33  obtain ⟨c, rfl⟩ := hf34  obtain ⟨d, rfl⟩ := hg35  rw [stepCombination_eq_sum, stepCombination_eq_sum]36  simp_rw [Finset.sum_mul, Finset.mul_sum]37  apply Submodule.sum_mem38  intro i _hi39  apply Submodule.sum_mem40  intro j _hj41  rw [smul_mul_smul_comm, initialStep_mul]42  exact Submodule.smul_mem _ _ (initialStep_mem_stepSpan _)4344/-- Add constants after extending the finite step functions by zero at infinity. -/45noncomputable def stepAlgebra : Subalgebra ℝ C(OnePoint ι, ℝ) where46  carrier := {f | ∃ r : ℝ, ∃ g : C₀(ι, ℝ), g ∈ stepSpan ∧47    f = ContinuousMap.const (OnePoint ι) r + g.toOnePoint}48  algebraMap_mem' r := by49    refine ⟨r, 0, Submodule.zero_mem _, ?_⟩50    simp51    ext x52    rfl53  zero_mem' := by54    refine ⟨0, 0, Submodule.zero_mem _, ?_⟩55    simp56  add_mem' := by57    rintro f h ⟨r, g, hg, rfl⟩ ⟨s, k, hk, rfl⟩58    refine ⟨r + s, g + k, Submodule.add_mem _ hg hk, ?_⟩59    ext x60    simp61    ring62  one_mem' := by63    refine ⟨1, 0, Submodule.zero_mem _, ?_⟩64    simp65  mul_mem' := by66    rintro f h ⟨r, g, hg, rfl⟩ ⟨s, k, hk, rfl⟩67    refine ⟨r * s, r • k + s • g + g * k, ?_, ?_⟩68    · exact Submodule.add_mem _69        (Submodule.add_mem _ (Submodule.smul_mem _ _ hk) (Submodule.smul_mem _ _ hg))70        (stepSpan_mul_mem g k hg hk)71    · ext x72      simp73      ring7475theorem initialStep_toOnePoint_mem_stepAlgebra (i : ι) :76    (initialStep i).toOnePoint ∈ (stepAlgebra : Subalgebra ℝ C(OnePoint ι, ℝ)) := by77  refine ⟨0, initialStep i, initialStep_mem_stepSpan i, ?_⟩78  simp7980theorem stepAlgebra_separatesPoints : (stepAlgebra : Subalgebra ℝ C(OnePoint ι, ℝ)).SeparatesPoints := by81  intro x y hxy82  have hsep (i : ι) (hi : (initialStep i).toOnePoint x ≠ (initialStep i).toOnePoint y) :83      ∃ f ∈ (fun f : C(OnePoint ι, ℝ) => (f : OnePoint ι → ℝ)) ''84        (stepAlgebra (ι := ι) : Set C(OnePoint ι, ℝ)), f x ≠ f y := by85    refine ⟨((initialStep i).toOnePoint : OnePoint ι → ℝ), ?_, hi⟩86    exact Set.mem_image_of_mem _ (initialStep_toOnePoint_mem_stepAlgebra i)87  induction x using OnePoint.rec with88  | infty =>89    induction y using OnePoint.rec with90    | infty => exact (hxy rfl).elim91    | coe j => apply hsep j; simp92  | coe i =>93    induction y using OnePoint.rec with94    | infty => apply hsep i; simp95    | coe j =>96      have hij : i ≠ j := fun h => hxy (congrArg (fun z : ι => (z : OnePoint ι)) h)97      rcases lt_or_gt_of_ne hij with hij | hji98      · apply hsep i99        simp [not_le.mpr hij]100      · apply hsep j101        simp [not_le.mpr hji]102103theorem stepCombination_denseRange : DenseRange (stepCombination : (ι →₀ ℝ) → C₀(ι, ℝ)) := by104  apply Metric.denseRange_iff.mpr105  intro f ε hε106  obtain ⟨h, hh⟩ := ContinuousMap.exists_mem_subalgebra_near_continuousMap_of_separatesPoints107    stepAlgebra stepAlgebra_separatesPoints f.toOnePoint (ε / 3) (by linarith)108  obtain ⟨r, g, hg, he⟩ := h.property109  obtain ⟨c, rfl⟩ := hg110  refine ⟨c, ?_⟩111  have hr : |r| < ε / 3 := by112    have hinf := (h.val - f.toOnePoint).norm_coe_le_norm (OnePoint.infty : OnePoint ι)113    have hinf' : |r| ≤ ‖h.val - f.toOnePoint‖ := by114      simpa [he] using hinf115    exact hinf'.trans_lt hh116  have hnorm : ‖stepCombination c - f‖ ≤ 2 * (ε / 3) := by117    apply c0_norm_le _ _ (by linarith)118    intro i119    have hp := (h.val - f.toOnePoint).norm_coe_le_norm (i : OnePoint ι)120    have hp' : |r + stepCombination c i - f i| < ε / 3 := by121      have h₁ : |r + stepCombination c i - f i| ≤ ‖h.val - f.toOnePoint‖ := by122        simpa [he] using hp123      exact h₁.trans_lt hh124    change |stepCombination c i - f i| ≤ 2 * (ε / 3)125    have h₁ := abs_le.mp hp'.le126    have h₂ := abs_le.mp hr.le127    exact abs_le.mpr ⟨by linarith, by linarith⟩128  rw [dist_comm, dist_eq_norm]129  exact hnorm.trans_lt (by linarith)130131end BFPP

SHA-256