GroupSampling.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Shared group sampling

The one-scale estimator in Section 5 is a finite uniform average. Its concentration follows from the explicitly cited Bernstein input. Choosing among representatives and extending their costs by cones is deterministic on the simultaneous approximation event, even when their samples are shared.

def OAI.EditApproximation.normalizedChildSample line 18

theorem OAI.EditApproximation.normalizedChildSample_moments line 24

Source documentation

The normalized sample bounds used by the executable group estimator follow from the rounded action's child bounds and the band sum guard.

theorem normalizedChildSample_moments {M : ℕ} (hM : 0 < M)
    (b h F : ℝ) (hb : 0 < b) (hh : 0 < h)
    (childScale childValue : Fin M → ℝ)
    (hscale : ∀ i, 0 ≤ childScale i)
    (hvalue : ∀ i, 0 ≤ childValue i ∧ childValue i ≤ 2 * childScale i)
    (hsum : (∑ i, childScale i) ≤ 64 * F * b) :
    (∀ i, 0 ≤ normalizedChildSample b h childScale childValue i ∧
      normalizedChildSample b h childScale childValue i ≤ 2 * ((M : ℝ) * h / b)) ∧
    uniformMean (normalizedChildSample b h childScale childValue) ≤ 128 * F := by
…

Mentions: OAI.EditApproximation.normalizedChildSample, OAI.EditApproximation.uniformMean

theorem OAI.EditApproximation.group_bernstein_exponent line 72
theorem OAI.EditApproximation.group_scale_concentration line 88

theorem OAI.EditApproximation.group_failure_union_bound line 110

Source documentation

Shared draws may correlate all representatives. The simultaneous event uses only finite subadditivity.

theorem group_failure_union_bound {Ω ι κ : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsFiniteMeasure μ] (members : Finset ι) (scales : Finset κ)
    (bad : ι → κ → Set Ω) (failure : ℝ)
    (hfailure : ∀ i ∈ members, ∀ h ∈ scales, μ.real (bad i h) ≤ failure) :
    μ.real (⋃ i ∈ members, ⋃ h ∈ scales, bad i h) ≤
      (members.card : ℝ) * scales.card * failure := by
…

theorem OAI.EditApproximation.group_scale_errors_sum line 125

theorem OAI.EditApproximation.selected_group_cost_le line 138

Source documentation

Estimated-cost minimization followed by actual evaluation loses at most twice the uniform estimation error. There is no probabilistic independence premise in this selection step.

theorem selected_group_cost_le {ι : Type*} (members : Finset ι)
    (cost estimate : ι → ℝ) (selected specified : ι) (error : ℝ)
    (hselected : selected ∈ members) (hspecified : specified ∈ members)
    (haccurate : ∀ i ∈ members, |estimate i - cost i| ≤ error)
    (hmin : estimate selected ≤ estimate specified) :
    cost selected ≤ cost specified + 2 * error := by
…

theorem OAI.EditApproximation.selected_group_cone_bound line 148