Suprema.lean

1import Mathlib.Algebra.Order.Archimedean.Real.Basic2import Mathlib.Order.ConditionallyCompleteLattice.Indexed3import Mathlib.Tactic.Linarith45/-! # Uniform estimates for real suprema and infima -/67namespace BFPP89set_option autoImplicit false1011open Set1213universe u14variable {ι : Type u} [Nonempty ι]1516theorem abs_ciSup_sub_ciSup_le (f g : ι → ℝ)17    (hf : BddAbove (range f)) (hg : BddAbove (range g)) (d : ℝ)18    (h : ∀ i, |f i - g i| ≤ d) : |(⨆ i, f i) - ⨆ i, g i| ≤ d := by19  have hfg : (⨆ i, f i) ≤ (⨆ i, g i) + d := by20    apply ciSup_le21    intro i22    have hi := (abs_le.mp (h i)).223    have hgi := le_ciSup hg i24    linarith25  have hgf : (⨆ i, g i) ≤ (⨆ i, f i) + d := by26    apply ciSup_le27    intro i28    have hi := (abs_le.mp (h i)).129    have hfi := le_ciSup hf i30    linarith31  exact abs_le.mpr ⟨by linarith, by linarith⟩3233theorem abs_ciInf_sub_ciInf_le (f g : ι → ℝ)34    (hf : BddBelow (range f)) (hg : BddBelow (range g)) (d : ℝ)35    (h : ∀ i, |f i - g i| ≤ d) : |(⨅ i, f i) - ⨅ i, g i| ≤ d := by36  have hfg : (⨅ i, f i) - d ≤ ⨅ i, g i := by37    apply le_ciInf38    intro i39    have hi := (abs_le.mp (h i)).240    have hfi := ciInf_le hf i41    linarith42  have hgf : (⨅ i, g i) - d ≤ ⨅ i, f i := by43    apply le_ciInf44    intro i45    have hi := (abs_le.mp (h i)).146    have hgi := ciInf_le hg i47    linarith48  exact abs_le.mpr ⟨by linarith, by linarith⟩4950theorem ciSup_const_of_nonempty (r : ℝ) : (⨆ _ : ι, r) = r := by51  exact ciSup_const5253end BFPP

SHA-256