SamplingTransfer.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite sampling transfer

The finite family consists of sampled column sequences and one sign per sampled occurrence. Its cardinal is (2 * N)^m, including repeated columns. The common bad event is paid once. Moment and tail obligations are explicit mathematical hypotheses, not additional published inputs.

theorem OAI.JointDickman.finiteProbability_nonneg line 24
theorem OAI.JointDickman.finiteExpectation_nonneg line 29
theorem OAI.JointDickman.finiteExpectation_indicator_cs line 33
theorem OAI.JointDickman.finiteProbability_bad_family line 57

theorem OAI.JointDickman.finiteExpectation_transfer line 76

Source documentation

Finite Cauchy–Schwarz turns a tail estimate into an expectation estimate.

theorem finiteExpectation_transfer {J : Type*} [Fintype J]
    (w : Ω → ℝ) (hw : ∀ x, 0 ≤ w x) (hwone : (∑ x, w x) = 1)
    (X A : Ω → ℝ) (Z : J → Ω → ℝ) (G : Ω → Prop)
    (e u V t : ℝ) (hthreshold : 0 ≤ u + e) (hV : 0 ≤ V)
    (hdom : ∀ x, X x ≤ A x)
    (hgood : ∀ x, G x → ∃ j, X x ≤ Z j x + e)
    (htail : ∀ j, finiteProbability w (fun x => G x ∧ u < Z j x) ≤ t)
    (hmoment : finiteExpectation w (fun x => A x ^ 2) ≤ V) :
    finiteExpectation w X ≤ u + e +
      Real.sqrt (V * (finiteProbability w (fun x => ¬ G x) + (Fintype.card J : ℝ) * t)) := by
…

Mentions: OAI.JointDickman.finiteProbability, OAI.JointDickman.finiteExpectation

def OAI.JointDickman.kernelCutMaximum line 123
Source documentation
The unnormalized finite real sign-cut maximum.
```
noncomputable def kernelCutMaximum (K : ι → ι → ℝ) : ℝ :=
…
```
theorem OAI.JointDickman.kernelCutMaximum_le line 127
theorem OAI.JointDickman.kernelCutMaximum_nonneg line 135
theorem OAI.JointDickman.kernelCutMaximum_le_absolute_mass line 141
abbrev OAI.JointDickman.ColumnSample line 151
Source documentation
A sampled column sequence with a sign attached to each occurrence.
```
abbrev ColumnSample (m : ℕ) := (Fin m → ι) × (Fin m → Bool)
…
```
theorem OAI.JointDickman.card_columnSample line 154
def OAI.JointDickman.columnSampleResponse line 160
def OAI.JointDickman.columnSampleResidual line 164
theorem OAI.JointDickman.kernelCutMaximum_sample_bound line 168
def OAI.JointDickman.kernelCutNorm line 187
Source documentation
The manuscript's normalization divides the sign maximum by N.
```
noncomputable def kernelCutNorm (K : ι → ι → ℝ) : ℝ :=
…
```
def OAI.JointDickman.kernelAbsoluteMass line 190
def OAI.JointDickman.columnSampleNorm line 193
def OAI.JointDickman.samplingError line 196
theorem OAI.JointDickman.kernelCutNorm_le_absolute_mass line 200
theorem OAI.JointDickman.kernelCutNorm_sample_bound line 204

theorem OAI.JointDickman.randomMatrix_sampling_transfer line 223

Source documentation

Quantitative transfer from the finite family to the fully adaptive cut. The common bad-event mass appears only once in the final error.

theorem randomMatrix_sampling_transfer
    (w : Ω → ℝ) (hw : ∀ x, 0 ≤ w x) (hwone : (∑ x, w x) = 1)
    (K : Ω → ι → ι → ℝ) (G : Ω → Prop) (d Q u V t : ℝ)
    (m : ℕ) (hm : 0 < m) (hV : 0 ≤ V)
    (hthreshold : 0 ≤ u + samplingError (ι := ι) d Q m)
…

Mentions: OAI.JointDickman.samplingError

theorem OAI.JointDickman.finiteExpectation_div line 253
theorem OAI.JointDickman.kernelAbsoluteMass_sq_le_average_rows line 258
theorem OAI.JointDickman.kernelAbsoluteMass_second_moment line 273
def OAI.JointDickman.realizedSiteKernel line 295
Source documentation
Realizing a finite site kernel on one independent configuration.
```
def realizedSiteKernel (E : ι → ι → A → A → ℝ) (x : ι → A) (i j : ι) : ℝ :=
…
```

theorem OAI.JointDickman.realizedSiteKernel_second_moment line 300

Source documentation

The uniform-integrability moment required in the sampling transfer is derived from the row-moment theorem.

theorem realizedSiteKernel_second_moment
    (p : ι → A → ℝ) (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (E H : ι → ι → A → A → ℝ)
    (hdom : ∀ i j a b, |E i j a b| ≤ H i j a b)
    (hdiag : ∀ i a, H i i a a = 0) (C q : ℝ)
    (hmean : ∀ i a, |siteRowMean p H i a| ≤ C)
    (hsquare : ∀ i, (∑ j, finiteExpectation (siteProductMass p)
      (fun x => H i j (x i) (x j) ^ 2)) ≤ q) :
    finiteExpectation (siteProductMass p)
      (fun x => kernelAbsoluteMass (realizedSiteKernel E x) ^ 2) ≤ C ^ 2 + q := by
…

Mentions: OAI.JointDickman.siteRowMean, OAI.JointDickman.finiteExpectation, OAI.JointDickman.kernelAbsoluteMass, OAI.JointDickman.realizedSiteKernel

theorem OAI.JointDickman.siteKernel_sampling_transfer line 326

Source documentation

The finite quantitative transfer for actual independent site kernels. Only the finite family tail bound remains an explicit sampling obligation.

theorem siteKernel_sampling_transfer
    (p : ι → A → ℝ) (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (E H : ι → ι → A → A → ℝ) (G : (ι → A) → Prop)
    (hdom : ∀ i j a b, |E i j a b| ≤ H i j a b)
    (hdiag : ∀ i a, H i i a a = 0) (hsym : ∀ i j a b, E i j a b = E j i b a)
    (C q d Q u t : ℝ) (m : ℕ) (hm : 0 < m) (hq : 0 ≤ q)
    (hmean : ∀ i a, |siteRowMean p H i a| ≤ C)
    (hsquare : ∀ i, (∑ j, finiteExpectation (siteProductMass p)
      (fun x => H i j (x i) (x j) ^ 2)) ≤ q)
    (hthreshold : 0 ≤ u + samplingError (ι := ι) d Q m)
…

Mentions: OAI.JointDickman.siteRowMean, OAI.JointDickman.finiteExpectation, OAI.JointDickman.samplingError