SharedGroupInputBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A pathwise finite cover for every shared group estimator's current child inputs. Repeated samples and member uses are counted once.

theorem OAI.EditApproximation.groupQueriedChildLabels_card line 16
theorem OAI.EditApproximation.actual_group_input_in_cover line 26

theorem OAI.EditApproximation.groupCurrentInputCover_card line 45

Source documentation

One group and one envelope label use at most 624*M*Q*theta^-2 distinct current child inputs, on every seed and every sample outcome.

theorem groupCurrentInputCover_card {α : Type*} (source target : List α) {M b : ℕ}
    (parent : TargetInterval source.length) (exponent Q : ℕ) (cell : ℕ × ℕ) (h : ℚ)
    (hM : 0 < M) (hQ : 1 ≤ Q) (hb : 0 < b) (hh : 0 < h) (hfloor : (b : ℚ) / M ≤ h)
    (draw : Fin (groupSampleCount M Q b h) → Fin M) :
    ((groupCurrentInputCover source target parent b exponent Q cell h draw).card : ℚ) ≤
      624 * M * Q * ((2 : ℚ) ^ exponent) ^ 2 := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.groupSampleCount, OAI.EditApproximation.groupCurrentInputCover