SamplingConcentration.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Concentration after restriction to a common good event

The extension used in the manuscript's sampling argument is constructed explicitly from a finite good set. The only concentration hypothesis below is the uniform-constant finite-product specialization of McDiarmid's published bounded-differences inequality.

def OAI.JointDickman.goodSetExtension line 25

Source documentation

The finite McShane extension, clamped at the chosen upper bound.

noncomputable def goodSetExtension (G : Finset (ι → A)) (hG : G.Nonempty)
    (f : (ι → A) → ℝ) (c L : ℝ) (x : ι → A) : ℝ :=
…

theorem OAI.JointDickman.goodSetExtension_le line 29
theorem OAI.JointDickman.goodSetExtension_nonneg line 33
theorem OAI.JointDickman.goodSetExtension_eq line 42
theorem OAI.JointDickman.min_upper_add line 60
theorem OAI.JointDickman.goodSetExtension_lipschitz line 68
def OAI.JointDickman.finiteExpectation line 98
Source documentation
Expectation with respect to an explicitly supplied finite mass function.
```
noncomputable def finiteExpectation (w : Ω → ℝ) (f : Ω → ℝ) : ℝ :=
…
```
def OAI.JointDickman.finiteProbability line 102
Source documentation
Event mass for the same finite law.
```
noncomputable def finiteProbability (w : Ω → ℝ) (E : Ω → Prop) : ℝ :=
…
```
theorem OAI.JointDickman.finiteProbability_mono line 105
theorem OAI.JointDickman.finiteProbability_union_le line 115

theorem OAI.JointDickman.finiteProbability_union_on_good line 134

Source documentation

A common exceptional event is paid once, before the union over tests.

theorem finiteProbability_union_on_good {J : Type*} [Fintype J]
    (w : Ω → ℝ) (hw : ∀ x, 0 ≤ w x) (G : Ω → Prop) (E : J → Ω → Prop) :
    finiteProbability w (fun x => ∃ j, E j x) ≤
      finiteProbability w (fun x => ¬ G x) +
        ∑ j, finiteProbability w (fun x => G x ∧ E j x) := by
…

Mentions: OAI.JointDickman.finiteProbability

theorem OAI.JointDickman.goodSetExtension_mean_le line 159
def OAI.JointDickman.PublishedInputs.siteProductMass line 189
Source documentation
Independent site mass, retaining the actual coordinate laws.
```
noncomputable def siteProductMass {ι A : Type*} [Fintype ι]
    (p : ι → A → ℝ) (x : ι → A) : ℝ := ∏ i, p i (x i)
```
def OAI.JointDickman.PublishedInputs.FiniteMcDiarmidInput line 198
Source documentation
McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, Theorem (6.7), pp. 166–167 (proof p. 168), DOI 10.1017/CBO9781107359949.008. The one-sided estimate follows by applying that martingale theorem to the coordinate Doob martingale. Only independent finite sites and one common coordinate bound are needed. The global Hamming bound is a stronger sufficient hypothesis on f.
```
def FiniteMcDiarmidInput (ι A : Type*) [Fintype ι] [DecidableEq ι]
    [Fintype A] [DecidableEq A] : Prop :=
…
```
theorem OAI.JointDickman.abs_clamp_sub_clamp_le line 214

theorem OAI.JointDickman.goodSet_concentration line 219

Source documentation

A concentration bound valid on one common good event. The cost of the bad event enters the mean only once, before any later union bound.

theorem goodSet_concentration (hMC : PublishedInputs.FiniteMcDiarmidInput ι A)
    (p : ι → A → ℝ) (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (G : Finset (ι → A)) (hG : G.Nonempty) (Z : (ι → A) → ℝ)
    {c L u a : ℝ} (hc : 0 ≤ c) (hL : 0 ≤ L) (ha : 0 < a)
    (hZ : ∀ x, 0 ≤ Z x)
    (hlip : ∀ x ∈ G, ∀ y ∈ G, |Z x - Z y| ≤ c * hammingDist x y)
    (hmean : finiteExpectation (PublishedInputs.siteProductMass p) Z +
      L * finiteProbability (PublishedInputs.siteProductMass p) (fun x => x ∉ G) ≤ u)
    (hcut : u + a < L) :
    finiteProbability (PublishedInputs.siteProductMass p)
      (fun x => x ∈ G ∧ u + a < Z x) ≤
        Real.exp (-2 * a ^ 2 / ((Fintype.card ι : ℝ) * c ^ 2)) := by
…

Mentions: OAI.JointDickman.PublishedInputs.FiniteMcDiarmidInput, OAI.JointDickman.finiteExpectation, OAI.JointDickman.PublishedInputs.siteProductMass, OAI.JointDickman.finiteProbability

theorem OAI.JointDickman.column_abs_sum_sub_le line 264

theorem OAI.JointDickman.incident_change_mass_le line 276

Source documentation

Only edges incident to changed coordinates contribute to the response. The argument uses the two endpoint degree bounds directly, without a path of intermediate good configurations.

theorem incident_change_mass_le (K K' H : ι → ι → ℝ) (T : Finset ι)
    (hsym : ∀ i j, H i j = H j i) (hH : ∀ i j, 0 ≤ H i j)
    (d : ℝ) (hrow : ∀ i, (∑ j, H i j) ≤ d)
    (hbound : ∀ i j, |K i j - K' i j| ≤ H i j)
    (heq : ∀ i ∉ T, ∀ j ∉ T, K i j = K' i j) :
    (∑ j, ∑ i, |K i j - K' i j|) ≤ 2 * T.card * d := by
…

def OAI.JointDickman.siteColumnResponse line 314
Source documentation
The unnormalized residual column response for fixed single-site tests.
```
noncomputable def siteColumnResponse (E : ι → ι → A → A → ℝ)
    (g : ι → A → ℝ) (x : ι → A) : ℝ :=
…
```
theorem OAI.JointDickman.siteColumnResponse_lipschitz_on_good line 318