OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleCorrection.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionOracleDensity.integerPoint line 18
2. lemma OAI.ContingencyTables.CompanionOracleDensity.pull_integerPoint line 21
3. lemma OAI.ContingencyTables.CompanionOracleDensity.density_at_integer line 28

   Source documentation

   The continuous evaluator density at every integer assignment is the original summand defining the manuscript's h.

   lemma density_at_integer (A : Instance I J) (C a : ℝ) (hC : 0 < C)
       (z : View A → ℕ) (f : FreeIndex A.small A.T A.b) :
       rho A C a z (integerPoint A C f)=
         (2:ℝ)^(-(a*C/height A C)*ForestPenaltyBound.penalty A z f) := by
   …

   Mentions: OAI.ContingencyTables.CompanionOracleDensity.rho, OAI.ContingencyTables.CompanionOracleDensity.integerPoint, OAI.ContingencyTables.CompanionOracleDensity.height, OAI.ContingencyTables.ForestPenaltyBound.penalty

4. lemma OAI.ContingencyTables.CompanionOracleDensity.sum_density_integer line 42
5. def OAI.ContingencyTables.CompanionOracleDensity.integerBin line 51
6. def OAI.ContingencyTables.CompanionOracleDensity.integerFiber line 62
7. lemma OAI.ContingencyTables.CompanionOracleDensity.ownFiber_positive line 66
8. def OAI.ContingencyTables.CompanionOracleDensity.binSum line 72
9. lemma OAI.ContingencyTables.CompanionOracleDensity.binSum_positive line 75
10. def OAI.ContingencyTables.CompanionOracleDensity.assignmentCount line 81
11. lemma OAI.ContingencyTables.CompanionOracleDensity.assignmentCount_positive line 83
12. def OAI.ContingencyTables.CompanionOracleDensity.correctedMass line 87
13. def OAI.ContingencyTables.CompanionOracleDensity.correction line 92
14. lemma OAI.ContingencyTables.CompanionOracleDensity.corrected_mass_product line 99

    Source documentation

    Population correction cancels the bin size and bin weight exactly, before taking any expectation or approximation.

    lemma corrected_mass_product (A : Instance I J) (C a : ℝ) (z : View A → ℕ)
        (K : ℕ) (hK : 0 < K) (f : FreeIndex A.small A.T A.b) :
        correctedMass A C a z K hK f*correction A C a z K hK f=
          ((K:ℝ)^dimension A/(assignmentCount A*binSum A C a z K))*
            rho A C a z (integerPoint A C f) := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.correctedMass, OAI.ContingencyTables.CompanionOracleDensity.correction, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.CompanionOracleDensity.assignmentCount, OAI.ContingencyTables.CompanionOracleDensity.binSum, OAI.ContingencyTables.CompanionOracleDensity.rho, OAI.ContingencyTables.CompanionOracleDensity.integerPoint

15. theorem OAI.ContingencyTables.CompanionOracleDensity.corrected_expectation line 115

    Source documentation

    The exact corrected mean contains the literal original free-assignment sum, not a continuous integral or a surrogate count.

    theorem corrected_expectation (A : Instance I J) (C a : ℝ) (hC : 0 < C)
        (z : View A → ℕ) (K : ℕ) (hK : 0 < K) :
        (∑ f : FreeIndex A.small A.T A.b,
          correctedMass A C a z K hK f*correction A C a z K hK f)=
          ((K:ℝ)^dimension A/(assignmentCount A*binSum A C a z K))*
            h A (a*C/height A C) z := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.correctedMass, OAI.ContingencyTables.CompanionOracleDensity.correction, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.CompanionOracleDensity.assignmentCount, OAI.ContingencyTables.CompanionOracleDensity.binSum, OAI.ContingencyTables.CompanionOracleDensity.height

16. def OAI.ContingencyTables.CompanionOracleDensity.ratioObservable line 124
17. def OAI.ContingencyTables.CompanionOracleDensity.ratioMean line 128
18. lemma OAI.ContingencyTables.CompanionOracleDensity.floor_step line 132
19. theorem OAI.ContingencyTables.CompanionOracleDensity.ratioObservable_cases line 141

    Source documentation

    The actual phase observable takes exactly the two source values, since one annealing step changes its integer exponent by zero or one.

    theorem ratioObservable_cases (A : Instance I J) (C : ℝ) (hC : 0 < C)
        (a : ℕ) (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
        {K : ℕ} (hKB : (K:ℝ) ≤ binWidth A C) (v : Grid (I := Fin (dimension A)) K) :
    …

    Mentions: OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.dimension

20. lemma OAI.ContingencyTables.CompanionOracleDensity.ratioMean_eq line 179
21. lemma OAI.ContingencyTables.CompanionOracleDensity.binSum_zero line 194
22. lemma OAI.ContingencyTables.CompanionOracleDensity.ratio_telescope line 200
23. theorem OAI.ContingencyTables.CompanionOracleDensity.oracle_telescope line 214

    Source documentation

    The original h-value is exactly the product of the actual stationary ratio means and the integer-population correction mean.

    theorem oracle_telescope (A : Instance I J) (C : ℝ) (hC : 0 < C)
        (z : View A → ℕ) (K : ℕ) (hK : 0 < K) (j : ℕ) :
        (assignmentCount A:ℝ)*(∏ a∈Finset.range j,ratioMean A C a z K)*
          (∑ f : FreeIndex A.small A.T A.b,
            correctedMass A C j z K hK f*correction A C j z K hK f)=
          h A ((j:ℝ)*C/height A C) z := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.assignmentCount, OAI.ContingencyTables.CompanionOracleDensity.ratioMean, OAI.ContingencyTables.CompanionOracleDensity.correctedMass, OAI.ContingencyTables.CompanionOracleDensity.correction, OAI.ContingencyTables.CompanionOracleDensity.height