OAI/Combinatorics/ContingencyTables/Counting/CompanionCorrectionArithmetic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionOracleDensity.rationalIntegerPoint line 17
2. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalIntegerPoint_cast line 21
3. def OAI.ContingencyTables.CompanionOracleDensity.correctionExponent line 29
4. lemma OAI.ContingencyTables.CompanionOracleDensity.correctionExponent_cast line 34
5. theorem OAI.ContingencyTables.CompanionOracleDensity.correctionExponent_bounds line 44

   Source documentation

   The exponent passed to numerical approximation is a bounded rational, although the original capacities may be arbitrarily large.

   theorem correctionExponent_bounds (A : Instance I J) (C a : ℕ) (hC : 0 < C)
       (haH : a ≤ rationalHeight A C) (z : View A → ℕ)
       (K : ℕ) (hK : 0 < K) (hB : (K:ℝ)=binWidth A C) (f : FreeIndex A.small A.T A.b) :
       -2 ≤ correctionExponent A C a z K hK f ∧ correctionExponent A C a z K hK f ≤ 2 := by
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.correctionExponent

6. def OAI.ContingencyTables.CompanionOracleDensity.rationalPopulation line 67
7. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalPopulation_positive line 71
8. lemma OAI.ContingencyTables.CompanionOracleDensity.correction_eq_population_power line 78
9. def OAI.ContingencyTables.CompanionOracleDensity.computedCorrection line 99
10. theorem OAI.ContingencyTables.CompanionOracleDensity.computedCorrection_error line 106

    Source documentation

    A deterministic pointwise relative-error guarantee for the actual rational correction returned on every integer assignment.

    theorem computedCorrection_error (A : Instance I J) (C a : ℕ) (hC : 0 < C)
        (haH : a ≤ rationalHeight A C) (z : View A → ℕ)
        (K : ℕ) (hK : 0 < K) (hB : (K:ℝ)=binWidth A C)
        (sigma : ℚ) (hsigma : 0 < sigma) (f : FreeIndex A.small A.T A.b) :
        |(computedCorrection A C a z K hK sigma f:ℝ)-correction A C a z K hK f| ≤
          (sigma:ℝ)*correction A C a z K hK f := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.computedCorrection, OAI.ContingencyTables.CompanionOracleDensity.correction

11. theorem OAI.ContingencyTables.CompanionOracleDensity.computedCorrection_bounds line 123

    Source documentation

    Positivity and a uniform range hold on all executions, independently of the statistical event used by the estimator.

    theorem computedCorrection_bounds (A : Instance I J) (C a : ℕ) (hC : 0 < C)
        (haH : a ≤ rationalHeight A C) (z : View A → ℕ)
        (K : ℕ) (hK : 0 < K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
        (sigma : ℚ) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1/2)
        (f : FreeIndex A.small A.T A.b) :
        (1/16:ℝ) ≤ computedCorrection A C a z K hK sigma f ∧
          (computedCorrection A C a z K hK sigma f:ℝ) ≤ 8 := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.computedCorrection