DenseWeights.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Continuous and dyadic bin weights

The actual floor-rounded weights used by the dense grid sampler. Convexity of the penalty implies log-concavity of its density, and local changes of the scaled penalty give explicit comparisons with the dyadic bin weights.

def OAI.ContingencyTables.DenseWeights.density line 22
def OAI.ContingencyTables.DenseWeights.binWeight line 25
theorem OAI.ContingencyTables.DenseWeights.density_pos line 28
theorem OAI.ContingencyTables.DenseWeights.binWeight_pos line 31
theorem OAI.ContingencyTables.DenseWeights.binWeight_comparison line 35
Source documentation
Rounding the exponent down changes a weight by at most a factor two.
```
theorem binWeight_comparison {X : Type*} (A : ℝ) (p : X → ℝ) (v : X) :
    density A p v ≤ binWeight A p v ∧ binWeight A p v ≤ 2 * density A p v := by
…
```
Mentions: OAI.ContingencyTables.DenseWeights.density, OAI.ContingencyTables.DenseWeights.binWeight
theorem OAI.ContingencyTables.DenseWeights.density_le_binWeight line 49
Source documentation
A scaled-penalty change at most s gives the tube density bound.
```
theorem density_le_binWeight {X : Type*} (A : ℝ) (p : X → ℝ)
    (x v : X) (s : ℝ) (hchange : |A * p x - A * p v| ≤ s) :
    density A p x ≤ (2 : ℝ) ^ s * binWeight A p v := by
…
```
Mentions: OAI.ContingencyTables.DenseWeights.density, OAI.ContingencyTables.DenseWeights.binWeight
theorem OAI.ContingencyTables.DenseWeights.binWeight_le_density line 61
theorem OAI.ContingencyTables.DenseWeights.bin_density_comparison line 73
theorem OAI.ContingencyTables.DenseWeights.tube_density_comparison line 81
theorem OAI.ContingencyTables.DenseWeights.density_continuous line 88
theorem OAI.ContingencyTables.DenseWeights.density_logConcave line 94
Source documentation
The continuous density used by the sampler is log-concave on every convex domain on which its penalty is convex.
```
theorem density_logConcave {q : ℕ} (A : ℝ) (hA : 0 ≤ A)
    (p : PublishedInputs.Point q → ℝ) (K : Set (PublishedInputs.Point q))
    (hp : ConvexOn ℝ K p) : PublishedInputs.LogConcaveOn (density A p) K := by
…
```
Mentions: OAI.ContingencyTables.PublishedInputs.Point, OAI.ContingencyTables.PublishedInputs.LogConcaveOn, OAI.ContingencyTables.DenseWeights.density