OAI/Combinatorics/EditApproximation/Geometry/Accuracy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.integerAnswer line 19

   Source documentation

   The implementation clamps to the input length and rounds down.

   noncomputable def integerAnswer (N : ℕ) (value : ℝ) : ℕ :=
   …

2. theorem OAI.EditApproximation.integerAnswer_spec line 24

   Source documentation

   Clamping and rounding down preserve a one-sided approximation of an integer distance. This does not assert that an estimator has that bound.

   theorem integerAnswer_spec {N D : ℕ} {value ε : ℝ}
       (hDN : D ≤ N) (hε : 0 ≤ ε)
       (hlower : (D : ℝ) ≤ value) (hupper : value ≤ (1 + ε) * D) :
       D ≤ integerAnswer N value ∧
         (integerAnswer N value : ℝ) ≤ (1 + ε) * D := by
   …

   Mentions: OAI.EditApproximation.integerAnswer

3. theorem OAI.EditApproximation.integerAnswer_zero line 38
4. def OAI.EditApproximation.goodExcess line 42

   Source documentation

   The positive excess on executions having a good seed.

   noncomputable def goodExcess {Ω : Type*} (G : Set Ω) (value : Ω → ℝ) (D : ℕ) :
       Ω → ℝ := G.indicator (fun ω => max (value ω - D) 0)

5. theorem OAI.EditApproximation.goodExcess_nonneg line 45
6. theorem OAI.EditApproximation.goodExcess_tail line 52

   Source documentation

   Markov's inequality converts the positive-excess expectation bound of Section 8 into an approximation tail bound.

   theorem goodExcess_tail {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsFiniteMeasure μ]
       {G : Set Ω} {value : Ω → ℝ} {D : ℕ} {ℓ ε : ℝ}
       (hD : 0 < D) (hℓ : 0 < ℓ) (hε : 0 < ε)
       (hint : Integrable (goodExcess G value D) μ)
       (hmoment : (∫ ω, goodExcess G value D ω ∂μ) ≤ (D : ℝ) / ℓ) :
       μ.real {ω | ε * D ≤ goodExcess G value D ω} ≤ 1 / (ℓ * ε) := by
   …

   Mentions: OAI.EditApproximation.goodExcess

7. theorem OAI.EditApproximation.final_answer_accuracy line 73

   Source documentation

   Final probability assembly, with the two genuinely unresolved algorithmic guarantees exposed: a good-seed event and its excess moment. The stronger success probability 4/5 implies the paper's 2/3.

   theorem final_answer_accuracy {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ]
       {G : Set Ω} {value : Ω → ℝ} {N D : ℕ} {ℓ ε : ℝ}
       (hvalue : Measurable value) (hDN : D ≤ N) (hD : 0 < D)
       (hℓ : 0 < ℓ) (hε : 0 < ε) (haccuracy : 10 ≤ ℓ * ε)
       (hseed : μ.real Gᶜ ≤ 1 / 10)
       (hlower : ∀ ω ∈ G, (D : ℝ) ≤ value ω)
       (hint : Integrable (goodExcess G value D) μ)
       (hmoment : (∫ ω, goodExcess G value D ω ∂μ) ≤ (D : ℝ) / ℓ) :
       (4 / 5 : ℝ) ≤ μ.real {ω | D ≤ integerAnswer N (value ω) ∧
         (integerAnswer N (value ω) : ℝ) ≤ (1 + ε) * D} := by
   …

   Mentions: OAI.EditApproximation.goodExcess, OAI.EditApproximation.integerAnswer