OAI/Combinatorics/EditApproximation/Coarse/CoarseGlobalSeed.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous seed failure with the computed parameters

The count includes every dyadic guess, complete coarse-tree node and shift. Independent finite entry streams realize the actual full table law. Symbolic recursion indices carry exact equalities to the computed parameters.

  1. theorem OAI.EditApproximation.twice_square_le_two_pow line 20
  2. theorem OAI.EditApproximation.computed_coarse_B_upper line 27
  3. theorem OAI.EditApproximation.computed_coarse_height_large line 44
  4. theorem OAI.EditApproximation.coarseInternalNodes_add_one_le_pow line 51
  5. def OAI.EditApproximation.coarseEntryTailCount line 61

    Source documentation

    Multiplicity of all local Bernstein tails for one complete entry.

    def coarseEntryTailCount (B D n : ℕ) : ℕ :=
…
  6. theorem OAI.EditApproximation.computed_coarseEntryTailCount line 64
  7. theorem OAI.EditApproximation.computed_coarse_tail_exponent line 104
  8. theorem OAI.EditApproximation.coarse_global_exponential_failure line 114
  9. theorem OAI.EditApproximation.computed_initialAccuracy_failure line 146

    Source documentation

    Symbolic recursion indices prevent irrelevant normalization of integer logarithms in dependent draw types. The equalities retain the exact computed algorithm, rather than replacing it with a larger or assumed seed contract.

    theorem computed_initialAccuracy_failure (N B D : ℕ)
    [NeZero B] [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (hB : B = (integerParameters N).B)
    {α : Type*} [DecidableEq α] (x y : List α)
    (hD : D = computedCoarseDepth N (coarseEntryWidth x y))
    (hN : 0 < N) (hwidth : coarseEntryWidth x y ≤ N)
    (hell : 200 ≤ inputSmallLog N)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (coarseInitialMeasure B D (coarseEntryWidth x y)).real
      {draws | ¬ CoarseInitialAccuracyEvent B D (initialThresholdQ N) (initialLambda N) x y draws} ≤
      (2 : ℝ) ^ (4 * inputHeight N + 4) * Real.exp (-(inputHeight N : ℝ) ^ 3 / 768) := by
…

    Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseInitialMeasure, OAI.EditApproximation.CoarseInitialAccuracyEvent, OAI.EditApproximation.initialThresholdQ, OAI.EditApproximation.initialLambda, OAI.EditApproximation.inputHeight

  10. instance OAI.EditApproximation.coarseFullSeedMeasure_isProbabilityMeasure line 195
  11. def OAI.EditApproximation.CoarseFullSeedAccuracyEvent line 202
  12. theorem OAI.EditApproximation.computed_fullSeed_failure line 209

    Source documentation

    The full finite table law fails with probability below one percent. The cardinal bound is supplied by the actual labeled state-domain count.

    theorem computed_fullSeed_failure (N B : ℕ) [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    {I α : Type*} [Fintype I] [DecidableEq α] (depth : I → ℕ)
    (x y : I → List α) (hB : B = (integerParameters N).B)
    (hD : ∀ i, depth i = computedCoarseDepth N (coarseEntryWidth (x i) (y i)))
    (hN : 0 < N) (hwidth : ∀ i, coarseEntryWidth (x i) (y i) ≤ N)
    (hcount : Fintype.card I ≤ 2 ^ (5 * inputHeight N))
    (hell : 200 ≤ inputSmallLog N)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (coarseFullSeedMeasure B depth x y).real
      {draws | ¬ CoarseFullSeedAccuracyEvent N B depth x y draws} < 1 / 100 := by
…

    Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseFullSeedMeasure, OAI.EditApproximation.CoarseFullSeedAccuracyEvent

  13. theorem OAI.EditApproximation.computed_fullSeedTable_pathwise line 267

    Source documentation

    The executable full integer table uses exactly the supplied recursion indices. Computed-parameter equalities appear only in its correctness proofs.

    theorem computed_fullSeedTable_pathwise (N B : ℕ) {I α : Type*} [DecidableEq α]
    (depth : I → ℕ) (x y : I → List α) (hB : B = (integerParameters N).B)
    (hD : ∀ i, depth i = computedCoarseDepth N (coarseEntryWidth (x i) (y i)))
    (hN : 0 < N) (hwidth : ∀ i, coarseEntryWidth (x i) (y i) ≤ N)
    (hell : 200 ≤ inputSmallLog N) (draws : CoarseFullSeedDraws B depth x y)
    (hevent : CoarseFullSeedAccuracyEvent N B depth x y draws) :
    ∀ i, EditDistortion.edit (x i) (y i) ≤ coarseFullSeedTable N B depth x y draws i ∧
      coarseFullSeedTable N B depth x y draws i ≤
        (integerParameters N).initialFactor * EditDistortion.edit (x i) (y i) := by
…

    Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.CoarseFullSeedDraws, OAI.EditApproximation.CoarseFullSeedAccuracyEvent, OAI.EditDistortion.edit, OAI.EditApproximation.coarseFullSeedTable

  14. theorem OAI.EditApproximation.computed_fullSeedTable_range_zero line 282

    Source documentation

    Every actual table value is clamped, and all zero-cost entries remain zero even on executions outside the simultaneous accuracy event.

    theorem computed_fullSeedTable_range_zero (N B : ℕ) {I α : Type*} [DecidableEq α]
    (depth : I → ℕ) (x y : I → List α) (draws : CoarseFullSeedDraws B depth x y) :
    ∀ i, coarseFullSeedTable N B depth x y draws i ≤ N ∧
      (EditDistortion.edit (x i) (y i) = 0 → coarseFullSeedTable N B depth x y draws i = 0) := by
…

    Mentions: OAI.EditApproximation.CoarseFullSeedDraws, OAI.EditApproximation.coarseFullSeedTable, OAI.EditDistortion.edit

  15. theorem OAI.EditApproximation.computed_fullSeedTable_accuracy line 291

    Source documentation

    Simultaneous finite table accuracy under the scalar Bernstein hypothesis.

    theorem computed_fullSeedTable_accuracy (N B : ℕ) [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    {I α : Type*} [Fintype I] [DecidableEq α] (depth : I → ℕ) (x y : I → List α)
    (hB : B = (integerParameters N).B)
    (hD : ∀ i, depth i = computedCoarseDepth N (coarseEntryWidth (x i) (y i)))
    (hN : 0 < N) (hwidth : ∀ i, coarseEntryWidth (x i) (y i) ≤ N)
    (hcount : Fintype.card I ≤ 2 ^ (5 * inputHeight N))
    (hell : 200 ≤ inputSmallLog N)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (coarseFullSeedMeasure B depth x y).real {draws | ¬ ∀ i,
      EditDistortion.edit (x i) (y i) ≤ coarseFullSeedTable N B depth x y draws i ∧
…

    Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.computedCoarseDepth, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.inputHeight, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseFullSeedMeasure, OAI.EditDistortion.edit, OAI.EditApproximation.coarseFullSeedTable