GridMeasure.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Volume and mass of grid face neighbourhoods

The exact tube volume and a finite integral-cover bound used to turn the interpolation shell gain into a weighted cut estimate.

def OAI.ContingencyTables.GridBoundary.tubeLower line 24
def OAI.ContingencyTables.GridBoundary.tubeUpper line 27
def OAI.ContingencyTables.GridBoundary.faceTube line 31
Source documentation
An open rectangular neighbourhood of the positive i-face of a bin.
```
def faceTube (a : I → ℤ) (i : I) (r : ℝ) : Set (I → ℝ) :=
…
```
theorem OAI.ContingencyTables.GridBoundary.faceTube_measurable line 34
theorem OAI.ContingencyTables.GridBoundary.tube_width line 39
theorem OAI.ContingencyTables.GridBoundary.product_one_exception line 43
theorem OAI.ContingencyTables.GridBoundary.faceTube_volume line 51
theorem OAI.ContingencyTables.GridBoundary.faceTube_volume_toReal line 61
theorem OAI.ContingencyTables.GridBoundary.reverse_bernoulli line 66
theorem OAI.ContingencyTables.GridBoundary.faceTube_volume_le_one line 85
Source documentation
The manuscript's tube-volume bound follows without an exponential estimate: the relevant power is at most two by reverse Bernoulli.
```
theorem faceTube_volume_le_one (a : I → ℤ) (i : I) (r : ℝ)
    (hr : 0 ≤ r) (hr₁ : r ≤ 1 / 4)
    (hsize : (Fintype.card I - 1 : ℕ) * (2 * r) ≤ (1 / 2 : ℝ)) :
    (volume (faceTube a i r)).toReal ≤ 1 := by
…
```
Mentions: OAI.ContingencyTables.GridBoundary.faceTube
theorem OAI.ContingencyTables.GridBoundary.mem_faceTube_of_near line 97
Source documentation
A point near the positive face belongs to its rectangular tube.
```
theorem mem_faceTube_of_near (a : I → ℤ) (i : I) (r : ℝ) (z w : I → ℝ)
    (hw : ClosedBin a w) (hwi : w i = (a i : ℝ) + 1)
    (hd : ∀ j, |z j - w j| < r) : z ∈ faceTube a i r := by
…
```
Mentions: OAI.ContingencyTables.GridBoundary.ClosedBin, OAI.ContingencyTables.GridBoundary.faceTube

theorem OAI.ContingencyTables.integral_finite_cover line 120

Source documentation

Integrating a finite cover, allowing overlap and a null exceptional set. This applies to the face tubes after removing grid hyperplanes.

theorem integral_finite_cover {X K : Type*} [MeasurableSpace X] [Fintype K]
    {μ : Measure X} (S : Set X) (E : K → Set X) (ρ : X → ℝ)
    (hS : MeasurableSet S) (hE : ∀ k, MeasurableSet (E k))
    (hiS : IntegrableOn ρ S μ) (hiE : ∀ k, IntegrableOn ρ (E k) μ)
    (hpos : ∀ k x, x ∈ E k → 0 ≤ ρ x)
    (hcover : ∀ᵐ x ∂μ, x ∈ S → ∃ k, x ∈ E k) :
    (∫ x in S, ρ x ∂μ) ≤ ∑ k, ∫ x in E k, ρ x ∂μ := by
…