OAI/Combinatorics/KMedianRecovery/Refined/StateWeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual sampling-state weight bound and its first-stage and extended-state consequences.

  1. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.uncovered_weight line 11
  2. theorem OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.state_weight_bound line 42
  3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.near_mass_le line 137
  4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.first_total_weight line 158
  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.extended_total_weight line 172