Valid

formal source

  46, lo_le_hi := by have := C.eps_nonneg z; linarith }
  47
  48/-- Validity of a certificate w.r.t. a charge map `Z` and display function `Fgap`. -/
  49structure Valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) (C : AnchorCert Species) : Prop where
  50  M0_pos : 0 < C.M0.lo
  51  Fgap_in : ∀ i : Species, memI (Igap C (Z i)) (Fgap (Z i))
  52  Ires_in_Igap : ∀ i : Species,
  53    (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi
  54
  55lemma M0_pos_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  56    {C : AnchorCert Species} (hC : Valid Z Fgap C) : 0 < C.M0.lo :=
  57  hC.M0_pos
  58
  59/-- Certificate replacement for the anchor identity (inequality form). -/
  60lemma anchorIdentity_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
  61    {C : AnchorCert Species} (hC : Valid Z Fgap C)
  62  (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i)) :
  63  ∀ i : Species, |res i - Fgap (Z i)| ≤ 2 * C.eps (Z i) := by
  64  intro i
  65  have hF : memI (Igap C (Z i)) (Fgap (Z i)) := hC.Fgap_in i
  66  have hI : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
  67    hC.Ires_in_Igap i
  68  have hr : memI (Igap C (Z i)) (res i) := by
  69    have hr0 := hres i
  70    refine ⟨le_trans hI.1 hr0.1, le_trans hr0.2 hI.2⟩
  71  have hbound :=
  72    abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := Fgap (Z i)) hr hF
  73  -- width(Igap) = 2*eps
  74  have hw :
  75      width (Igap C (Z i)) = 2 * C.eps (Z i) := by
  76    simp [Igap, width]
  77    ring
  78  simpa [hw, two_mul] using hbound
  79