lemma
proved
tactic proof
equalZ_residue_of_cert
show as:
view Lean formalization →
formal statement (Lean)
81lemma equalZ_residue_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
82 {C : AnchorCert Species} (hC : Valid Z Fgap C)
83 (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i))
84 {i j : Species} (hZ : Z i = Z j) :
85 |res i - res j| ≤ 2 * C.eps (Z i) := by
proof body
Tactic-mode proof.
86 have hI_i : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
87 hC.Ires_in_Igap i
88 have hI_j : (Igap C (Z j)).lo ≤ (C.Ires j).lo ∧ (C.Ires j).hi ≤ (Igap C (Z j)).hi :=
89 hC.Ires_in_Igap j
90 have hres_i : memI (Igap C (Z i)) (res i) := by
91 have hr0 := hres i
92 exact ⟨le_trans hI_i.1 hr0.1, le_trans hr0.2 hI_i.2⟩
93 have hres_j : memI (Igap C (Z i)) (res j) := by
94 have hr0 := hres j
95 have hlo_j : (Igap C (Z i)).lo ≤ (C.Ires j).lo := by simpa [hZ] using hI_j.1
96 have hhi_j : (C.Ires j).hi ≤ (Igap C (Z i)).hi := by simpa [hZ] using hI_j.2
97 exact ⟨le_trans hlo_j hr0.1, le_trans hr0.2 hhi_j⟩
98 have hbound :=
99 abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := res j) hres_i hres_j
100 have hw :
101 width (Igap C (Z i)) = 2 * C.eps (Z i) := by
102 simp [Igap, width]
103 ring
104 simpa [hw, two_mul] using hbound
105
106/-! ### Zero-width anchor certificate (exact equality) -/
107
108/-- Zero-width certificate: each interval collapses to the center value `Fgap(Z i)`. -/