CompanionOracleJointLaw.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the actual bin-then-integer sampling law

lemma OAI.ContingencyTables.CompanionOracleDensity.sum_by_bins line 16
lemma OAI.ContingencyTables.CompanionOracleDensity.total_of_bin_sums line 24
theorem OAI.ContingencyTables.CompanionOracleDensity.correctedMass_nonnegative line 33
lemma OAI.ContingencyTables.CompanionOracleDensity.correctedMass_fiber_sum line 41
theorem OAI.ContingencyTables.CompanionOracleDensity.correctedMass_total line 67
Source documentation
Choosing a stationary bin and then an exactly uniform integer point in that bin defines a probability law on the actual free assignments.
```
theorem correctedMass_total (A : Instance I J) (C a : ℝ) (z : View A → ℕ)
    (K : ℕ) (hK : 0 < K) (hW : 100*A.d*K ≤ A.W) :
    (∑ f : FreeIndex A.small A.T A.b,correctedMass A C a z K hK f)=1 := by
…
```
Mentions: OAI.ContingencyTables.CompanionOracleDensity.correctedMass
lemma OAI.ContingencyTables.CompanionOracleDensity.integerPoint_distance line 76
theorem OAI.ContingencyTables.CompanionOracleDensity.correction_bounds line 100
Source documentation
The correction variable is uniformly bounded, independently of the success event and of the number of integers in a bin.
```
theorem correction_bounds (A : Instance I J) (C a : ℝ) (hC : 0 < C)
    (ha : 0 ≤ a) (haH : a ≤ height A C) (z : View A → ℕ)
    (K : ℕ) (hK : 0 < K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
    (f : FreeIndex A.small A.T A.b) :
    1/8 ≤ correction A C a z K hK f ∧ correction A C a z K hK f ≤ 4 := by
…
```
Mentions: OAI.ContingencyTables.CompanionOracleDensity.height, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.correction