StepFunctions.lean

1import BFPP.C0Profiles2import BFPP.FiniteSynthesis3import Mathlib.Topology.Algebra.Indicator4import Mathlib.LinearAlgebra.Finsupp.LinearCombination56/-! # Compactly supported initial-segment functions -/78namespace BFPP910set_option autoImplicit false1112open Set Order Filter Topology13open scoped ZeroAtInfty1415universe u16variable {ι : Type u} [LinearOrder ι] [OrderBot ι] [SuccOrder ι] [NoMaxOrder ι]17  [TopologicalSpace ι] [OrderTopology ι] [CompactIccSpace ι]1819theorem initialSegment_isClopen (i : ι) : IsClopen (Iic i) := by20  refine ⟨isClosed_Iic, ?_⟩21  have he : Iic i = Iio (Order.succ i) := by ext j; simp only [mem_Iic, mem_Iio, Order.lt_succ_iff]22  rw [he]23  exact isOpen_Iio2425theorem initialSegment_isCompact (i : ι) : IsCompact (Iic i) := by26  simpa only [Icc_bot] using (isCompact_Icc (a := (⊥ : ι)) (b := i))2728noncomputable def initialStep (i : ι) : C₀(ι, ℝ) where29  toFun := (Iic i).indicator (fun _ => 1)30  continuous_toFun := (initialSegment_isClopen i).continuous_indicator continuous_const31  zero_at_infty' := by32    have he : (fun _ : ι => (0 : ℝ)) =ᶠ[cocompact ι] (Iic i).indicator (fun _ => 1) := by33      filter_upwards [(initialSegment_isCompact i).compl_mem_cocompact] with j hj34      simp only [Set.indicator_of_notMem hj]35    exact tendsto_const_nhds.congr' he3637@[simp] theorem initialStep_apply (i j : ι) : initialStep i j = if j ≤ i then 1 else 0 := by38  classical39  change (Iic i).indicator (fun _ => (1 : ℝ)) j = _40  by_cases h : j ≤ i <;> simp [Set.indicator, h]4142noncomputable def c0Eval (i : ι) : C₀(ι, ℝ) →ₗ[ℝ] ℝ where43  toFun f := f i44  map_add' _ _ := rfl45  map_smul' _ _ := rfl4647theorem c0_abs_apply_le_norm (f : C₀(ι, ℝ)) (i : ι) : |f i| ≤ ‖f‖ := by48  change ‖f.toBCF i‖ ≤ ‖f.toBCF‖49  exact f.toBCF.norm_coe_le_norm i5051theorem c0_norm_le (f : C₀(ι, ℝ)) (C : ℝ) (hC : 0 ≤ C)52    (hf : ∀ i, |f i| ≤ C) : ‖f‖ ≤ C :=53  (BoundedContinuousFunction.norm_le hC).mpr hf5455theorem c0_abs_sub_le_dist (f g : C₀(ι, ℝ)) (i : ι) : |f i - g i| ≤ dist f g := by56  rw [dist_eq_norm]57  exact c0_abs_apply_le_norm (f - g) i5859noncomputable def stepCombination : (ι →₀ ℝ) →ₗ[ℝ] C₀(ι, ℝ) :=60  Finsupp.linearCombination ℝ initialStep6162theorem stepCombination_apply (c : ι →₀ ℝ) (i : ι) :63    stepCombination c i = stepFinsetValue c.support c i := by64  change c0Eval i (Finsupp.linearCombination ℝ initialStep c) = _65  rw [Finsupp.apply_linearCombination]66  simp only [Finsupp.linearCombination_apply, Finsupp.sum, Function.comp_apply,67    c0Eval, LinearMap.coe_mk, AddHom.coe_mk, initialStep_apply, smul_eq_mul,68    mul_ite, mul_one, mul_zero, stepFinsetValue]6970@[simp] theorem stepCombination_single (i : ι) :71    stepCombination (Finsupp.single i (1 : ℝ)) = initialStep i := by72  simp [stepCombination, Finsupp.linearCombination_single]7374end BFPP

SHA-256