English
From an estimator for a pair, extract an estimator for the first factor.
Русский
Из оценивателя пар извлечь оцениватель для первого множителя.
LaTeX
$$def fstInst ... : Estimator a (Estimator.fst (a.prod b) ε)$$
Lean4
/-- Given an estimator for a pair, we can extract an estimator for the first factor. -/
-- This isn't an instance as at the sole use case we need to provide
-- the instance arguments by hand anyway.
def fstInst [DecidableLT α] [∀ (p : α × β), WellFoundedGT { q // q ≤ p }] (a : Thunk α) (b : Thunk β)
(i : Estimator (a.prod b) ε) : Estimator a (Estimator.fst (a.prod b) ε)
where
bound_le e := (Estimator.bound_le e.inner : bound (a.prod b) e.inner ≤ (a.get, b.get)).1
improve_spec
e := by
let bd := (bound (a.prod b) e.inner).1
have := Estimator.improveUntil_spec (a.prod b) (fun p => bd < p.1) e.inner
revert this
simp only [EstimatorData.improve, decide_eq_true_eq]
match Estimator.improveUntil (a.prod b) _ _ with
| .error _ =>
simp only
exact fun w => eq_of_le_of_not_lt (Estimator.bound_le e.inner : bound (a.prod b) e.inner ≤ (a.get, b.get)).1 w
| .ok e' => exact fun w => w
