OAI/Combinatorics/ContingencyTables/Rooted/RootedCorrectionArithmetic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedOracleDensity.correctionExponent line 19
2. lemma OAI.ContingencyTables.RootedOracleDensity.correctionExponent_cast line 24
3. theorem OAI.ContingencyTables.RootedOracleDensity.correctionExponent_bounds line 34

   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) (R : RootedCompletion.Selection A.T) (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 R C a z K hK f ∧ correctionExponent A R C a z K hK f ≤ 2 := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedOracleDensity.correctionExponent

4. lemma OAI.ContingencyTables.RootedOracleDensity.correction_eq_population_power line 57
5. def OAI.ContingencyTables.RootedOracleDensity.computedCorrection line 78
6. theorem OAI.ContingencyTables.RootedOracleDensity.computedCorrection_error line 85

   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) (R : RootedCompletion.Selection A.T) (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 R C a z K hK sigma f:ℝ)-correction A R C a z K hK f| ≤
         (sigma:ℝ)*correction A R C a z K hK f := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedOracleDensity.computedCorrection, OAI.ContingencyTables.RootedOracleDensity.correction

7. theorem OAI.ContingencyTables.RootedOracleDensity.computedCorrection_bounds line 102

   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) (R : RootedCompletion.Selection A.T) (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 R C a z K hK sigma f ∧
         (computedCorrection A R C a z K hK sigma f:ℝ) ≤ 8 := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedOracleDensity.computedCorrection