TerminalNormalization.lean

1import BFPP.TerminalSupremum2import BFPP.BoundedFamilies3import Mathlib.Algebra.Order.GroupWithZero.OrderIso45/-! # Normalizing a discontinuous terminal supremum -/67namespace BFPP89set_option autoImplicit false10open Set unitInterval1112universe u v13variable {K : Type u} [TopologicalSpace K]1415noncomputable def boundedUnitFunction (f : K → I) : BoundedFamily K :=16  BoundedFamily.ofBound (fun t => (f t : ℝ)) 117    (fun t => by rw [Real.norm_eq_abs, abs_of_nonneg (f t).property.1]; exact (f t).property.2)1819theorem terminal_norm_pos (f : K → I) (hf : ¬ Continuous f) : 0 < ‖boundedUnitFunction f‖ := by20  by_contra h21  have hzero : ‖boundedUnitFunction f‖ = 0 := le_antisymm (le_of_not_gt h) (norm_nonneg _)22  have hv : ∀ t, (f t : ℝ) = 0 := by23    intro t24    have hb := (boundedUnitFunction f).abs_apply_le_norm t25    rw [hzero] at hb26    exact abs_nonpos_iff.mp hb27  have hc : Continuous (fun t => (f t : ℝ)) := by28    simp only [hv]29    exact continuous_const30  exact hf (hc.subtype_mk _)3132noncomputable def normalizedTerminal (f : K → I) : BoundedFamily K :=33  ‖boundedUnitFunction f‖⁻¹ • boundedUnitFunction f3435@[simp] theorem normalizedTerminal_apply (f : K → I) (t : K) :36    normalizedTerminal f t = ‖boundedUnitFunction f‖⁻¹ * (f t : ℝ) := rfl3738theorem normalizedTerminal_norm (f : K → I) (hf : ¬ Continuous f) :39    ‖normalizedTerminal f‖ = 1 := by40  have hr := terminal_norm_pos f hf41  letI : TopologicalSpace K := ⊥42  rw [normalizedTerminal, norm_smul, Real.norm_eq_abs,43    abs_of_pos (inv_pos.mpr hr), inv_mul_cancel₀ hr.ne']4445theorem normalizedTerminal_bounds (f : K → I) (hf : ¬ Continuous f) (t : K) :46    0 ≤ normalizedTerminal f t ∧ normalizedTerminal f t ≤ 1 := by47  have hr := terminal_norm_pos f hf48  rw [normalizedTerminal_apply]49  refine ⟨mul_nonneg (inv_nonneg.mpr hr.le) (f t).property.1, ?_⟩50  have hb : (f t : ℝ) ≤ ‖boundedUnitFunction f‖ :=51    ((le_abs_self _).trans ((boundedUnitFunction f).abs_apply_le_norm t))52  calc53    ‖boundedUnitFunction f‖⁻¹ * (f t : ℝ) ≤ ‖boundedUnitFunction f‖⁻¹ * ‖boundedUnitFunction f‖ :=54      mul_le_mul_of_nonneg_left hb (inv_nonneg.mpr hr.le)55    _ = 1 := inv_mul_cancel₀ hr.ne'5657theorem normalizedTerminal_not_continuous (f : K → I) (hf : ¬ Continuous f) :58    ¬ Continuous (fun t => normalizedTerminal f t) := by59  intro hc60  have he : (fun t => ‖boundedUnitFunction f‖ * normalizedTerminal f t) = fun t => (f t : ℝ) := by61    funext t62    rw [normalizedTerminal_apply, ← mul_assoc,63      mul_inv_cancel₀ (terminal_norm_pos f hf).ne', one_mul]64  have hc' : Continuous (fun t => (f t : ℝ)) := he ▸ continuous_const.mul hc65  exact hf (hc'.subtype_mk _)6667/-- Positive rescaling preserves every nonempty bounded pointwise supremum,68and hence all the limit and terminal identities in the appendix. -/69theorem positive_scale_ciSup {ι : Type v} [Nonempty ι] (a : ℝ) (ha : 0 < a)70    (g : ι → ℝ) (hg : BddAbove (range g)) : a * (⨆ i, g i) = ⨆ i, a * g i :=71  (OrderIso.mulLeft₀ a ha).map_ciSup hg7273theorem normalized_profile_bounds (f : K → I) (hf : ¬ Continuous f) (g : C(K, I))74    (hg : ∀ t, g t ≤ f t) (t : K) :75    0 ≤ ‖boundedUnitFunction f‖⁻¹ * (g t : ℝ) ∧76      ‖boundedUnitFunction f‖⁻¹ * (g t : ℝ) ≤ 1 := by77  have hr := (terminal_norm_pos f hf).le78  refine ⟨mul_nonneg (inv_nonneg.mpr hr) (g t).property.1, ?_⟩79  have hgt : (g t : ℝ) ≤ (f t : ℝ) := hg t80  exact (mul_le_mul_of_nonneg_left hgt (inv_nonneg.mpr hr)).trans81    (normalizedTerminal_bounds f hf t).28283theorem normalized_profile_continuous (f : K → I) (g : C(K, I)) :84    Continuous (fun t => ‖boundedUnitFunction f‖⁻¹ * (g t : ℝ)) :=85  continuous_const.mul (continuous_subtype_val.comp g.continuous)8687end BFPP

SHA-256