SamplingSkeleton.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

A small-column sampling skeleton

This is the deterministic part of sampling-skeleton in the manuscript. Sampling with replacement allows repeated columns; their multiplicities are retained in the row response. The number of distinct columns is at most the sample size. No probabilistic or cut-approximation hypothesis is assumed.

def OAI.JointDickman.responseSign line 23
Source documentation
The best-response sign, with the manuscript's convention at zero.
```
noncomputable def responseSign (x : ℝ) : ℝ := if 0 ≤ x then 1 else -1
```
theorem OAI.JointDickman.abs_responseSign line 25
theorem OAI.JointDickman.mul_responseSign line 29
theorem OAI.JointDickman.responseSign_pos_mul line 35
theorem OAI.JointDickman.responseSign_loss line 40
Source documentation
A mistaken best response costs at most twice its prediction error.
```
theorem responseSign_loss (x y : ℝ) :
    |x| - x * responseSign y ≤ 2 * |x - y| := by
…
```
Mentions: OAI.JointDickman.responseSign
theorem OAI.JointDickman.sum_abs_le_sqrt_card_mul_sum_sq line 52

theorem OAI.JointDickman.sum_responseSign_loss line 61

Source documentation

An L² approximation to the row sums gives an L¹ best-response loss.

theorem sum_responseSign_loss {ι : Type*} [Fintype ι] (r q : ι → ℝ) :
    (∑ i, |r i|) ≤ (∑ i, r i * responseSign (q i)) +
      2 * Real.sqrt ((Fintype.card ι : ℝ) * ∑ i, (r i - q i) ^ 2) := by
…

Mentions: OAI.JointDickman.responseSign

theorem OAI.JointDickman.expect_coordinate_product line 69
theorem OAI.JointDickman.expect_coordinate line 77
theorem OAI.JointDickman.expect_distinct_coordinates line 90

theorem OAI.JointDickman.expect_sample_sum_sq line 108

Source documentation

Independent, centered coordinate samples have no off-diagonal terms.

theorem expect_sample_sum_sq {J A : Type*} [Fintype J] [DecidableEq J] [Fintype A] [Nonempty A]
    (f : A → ℝ) (hf : (𝔼 a : A, f a) = 0) :
    (𝔼 σ : J → A, (∑ j, f (σ j)) ^ 2) =
      (Fintype.card J : ℝ) * (𝔼 a : A, f a ^ 2) := by
…

theorem OAI.JointDickman.expect_centered_sq line 127

Source documentation

The usual finite-population variance identity.

theorem expect_centered_sq {A : Type*} [Fintype A] [Nonempty A] (f : A → ℝ) :
    (𝔼 a : A, (f a - (𝔼 b : A, f b)) ^ 2) =
      (𝔼 a : A, f a ^ 2) - (𝔼 a : A, f a) ^ 2 := by
…

theorem OAI.JointDickman.expect_sample_mean_sq_le line 135

Source documentation

Mean-square error for independent uniform samples, with replacement.

theorem expect_sample_mean_sq_le {A : Type*} [Fintype A] [Nonempty A]
    (f : A → ℝ) (m : ℕ) (hm : 0 < m) :
    (𝔼 σ : Fin m → A,
      ((∑ j, f (σ j)) / m - (𝔼 a : A, f a)) ^ 2) ≤
        (𝔼 a : A, f a ^ 2) / m := by
…

theorem OAI.JointDickman.exists_column_sample_sq_le line 161

Source documentation

The column estimator approximates every row simultaneously in squared error.

theorem exists_column_sample_sq_le {ι : Type*} [Fintype ι] [Nonempty ι]
    (K : ι → ι → ℝ) (δ : ι → ℝ) (hδ : ∀ j, |δ j| = 1)
    (m : ℕ) (hm : 0 < m) :
    ∃ σ : Fin m → ι,
      (∑ i, ((∑ j, K i j * δ j) -
        (Fintype.card ι : ℝ) / m * ∑ a, K i (σ a) * δ (σ a)) ^ 2) ≤
          (Fintype.card ι : ℝ) / m * ∑ i, ∑ j, K i j ^ 2 := by
…

theorem OAI.JointDickman.delete_endpoints_bound line 206

Source documentation

Removing a set of indices costs at most its row and column mass.

theorem delete_endpoints_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    (K : ι → ι → ℝ) (hsym : ∀ i j, K i j = K j i)
    (d : ℝ) (hrow : ∀ i, (∑ j, |K i j|) ≤ d)
    (T : Finset ι) (f g : ι → ℝ)
    (hf : ∀ i, |f i| ≤ 1) (hg : ∀ i, |g i| ≤ 1) :
    realBilinear K f g ≤
      (∑ i ∈ univ \ T, ∑ j ∈ univ \ T, K i j * f i * g j) +
        2 * T.card * d := by
…

Mentions: OAI.JointDickman.realBilinear

def OAI.JointDickman.sampledResponse line 257

Source documentation

The response obtained from an ordered sample of columns.

noncomputable def sampledResponse {ι : Type*} {m : ℕ}
    (K : ι → ι → ℝ) (δ : ι → ℝ) (σ : Fin m → ι) (i : ι) : ℝ :=
…

def OAI.JointDickman.residualColumnBound line 262

Source documentation

The residual column optimum after deleting the sampled endpoints.

noncomputable def residualColumnBound {ι : Type*} [Fintype ι] [DecidableEq ι]
    (K : ι → ι → ℝ) (T : Finset ι) (g : ι → ℝ) : ℝ :=
…

theorem OAI.JointDickman.exists_sampled_response_bound line 267

Source documentation

A fixed column-sign vector has a small-column best response with explicit loss.

theorem exists_sampled_response_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    [Nonempty ι] (K : ι → ι → ℝ) (hsym : ∀ i j, K i j = K j i)
    (d : ℝ) (hrow : ∀ i, (∑ j, |K i j|) ≤ d)
    (δ : ι → ℝ) (hδ : ∀ j, |δ j| = 1) (m : ℕ) (hm : 0 < m) :
    ∃ σ : Fin m → ι,
      (∑ i, |∑ j, K i j * δ j|) ≤
        residualColumnBound K (univ.image σ) (sampledResponse K δ σ) +
        2 * Real.sqrt ((Fintype.card ι : ℝ) *
          ((Fintype.card ι : ℝ) / m * ∑ i, ∑ j, K i j ^ 2)) + 2 * m * d := by
…

Mentions: OAI.JointDickman.residualColumnBound, OAI.JointDickman.sampledResponse

theorem OAI.JointDickman.exists_small_column_skeleton line 319

Source documentation

A single sampled response controls every sign cut of a symmetric matrix. The witness depends only on the matrix and uses at most m distinct columns.

theorem exists_small_column_skeleton {ι : Type*} [Fintype ι] [DecidableEq ι]
    [Nonempty ι] (K : ι → ι → ℝ) (hsym : ∀ i j, K i j = K j i)
    (d : ℝ) (hrow : ∀ i, (∑ j, |K i j|) ≤ d) (m : ℕ) (hm : 0 < m) :
    ∃ δ : ι → Bool, ∃ σ : Fin m → ι,
      (univ.image σ).card ≤ m ∧ ∀ s t : ι → Bool,
        |realBilinear K (fun i => cutSign (s i)) (fun j => cutSign (t j))| ≤
          residualColumnBound K (univ.image σ)
            (sampledResponse K (fun j => cutSign (δ j)) σ) +
          2 * Real.sqrt ((Fintype.card ι : ℝ) *
            ((Fintype.card ι : ℝ) / m * ∑ i, ∑ j, K i j ^ 2)) + 2 * m * d := by
…

Mentions: OAI.JointDickman.realBilinear, OAI.JointDickman.cutSign, OAI.JointDickman.residualColumnBound, OAI.JointDickman.sampledResponse