EnvelopeOrder.lean

1import BFPP.Envelopes23/-! # Order estimates for tail envelopes -/45namespace BFPP67set_option autoImplicit false8open Set910variable {ι : Type*} [Preorder ι]1112theorem lowerTail_le_point (f : BoundedFamily ι) (b j : ι) (hj : b ≤ j) :13    lowerTail f b ≤ f j :=14  ciInf_le (BoundedFamily.bddBelow_range (BoundedFamily.reindex (fun k : Ici b => k.val) f)) ⟨j, hj⟩1516theorem point_le_upperTail (f : BoundedFamily ι) (b j : ι) (hj : b ≤ j) :17    f j ≤ upperTail f b :=18  le_ciSup (BoundedFamily.bddAbove_range (BoundedFamily.reindex (fun k : Ici b => k.val) f)) ⟨j, hj⟩1920theorem le_lowerTail (f : BoundedFamily ι) (b : ι) (c : ℝ)21    (h : ∀ j, b ≤ j → c ≤ f j) : c ≤ lowerTail f b := by22  letI : Nonempty (Ici b) := ⟨⟨b, le_rfl⟩⟩23  exact le_ciInf (fun j => h j.val j.property)2425theorem upperTail_le (f : BoundedFamily ι) (b : ι) (c : ℝ)26    (h : ∀ j, b ≤ j → f j ≤ c) : upperTail f b ≤ c := by27  letI : Nonempty (Ici b) := ⟨⟨b, le_rfl⟩⟩28  exact ciSup_le (fun j => h j.val j.property)2930theorem lowerTail_le_lowerEnvelope (f : BoundedFamily ι) (b : ι) :31    lowerTail f b ≤ lowerEnvelope f := le_ciSup (lowerTails f).bddAbove_range b3233theorem upperEnvelope_le_upperTail (f : BoundedFamily ι) (b : ι) :34    upperEnvelope f ≤ upperTail f b := ciInf_le (upperTails f).bddBelow_range b3536theorem lowerEnvelope_le [Nonempty ι] (f : BoundedFamily ι) (c : ℝ)37    (h : ∀ b, lowerTail f b ≤ c) : lowerEnvelope f ≤ c := ciSup_le h3839theorem le_upperEnvelope [Nonempty ι] (f : BoundedFamily ι) (c : ℝ)40    (h : ∀ b, c ≤ upperTail f b) : c ≤ upperEnvelope f := le_ciInf h4142end BFPP

SHA-256