Rounding.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

High-value rounding of finite nonnegative vectors. The finite threshold partition and bounded shared rejection sampler produce an ordinary deterministic labeling. The auxiliary edge sample may retain hidden constraint information; the labeling receives only its local vertex.

theorem OAI.MaxCutGames.Repetition.threshold_average_good_mass line 26
theorem OAI.MaxCutGames.Repetition.exists_labeling_high_value line 43
Source documentation
Unit squared row mass converts a large collision energy into a genuinely local deterministic labeling. All randomness used by the proof is independent of the sampled constraint, and the final answer has no random seed.
```
theorem exists_labeling_high_value (ν : FiniteDistribution E)
    (left right : E → V) (R : E → A → A → Bool)
    (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v = 1) :
    ∃ labels : V → A,
      1 - 2 * Real.sqrt (2 * (1 - pairEnergy ν left right R a f)) ≤
        partialLabelScore ν left right R labels := by
…
```
Mentions: OAI.MaxCutGames.Repetition.rowSquareMass, OAI.MaxCutGames.Repetition.pairEnergy, OAI.MaxCutGames.Repetition.partialLabelScore

theorem OAI.MaxCutGames.Repetition.exists_labeling_high_value_of_rows_le_one line 63

Source documentation

Rows of mass at most one are completed by private vertex coordinates. Their nonnegative contribution only improves the collision energy.

theorem exists_labeling_high_value_of_rows_le_one (ν : FiniteDistribution E)
    (left right : E → V) (R : E → A → A → Bool)
    (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v ≤ 1) :
    ∃ labels : V → A,
      1 - 2 * Real.sqrt (2 * (1 - pairEnergy ν left right R a f)) ≤
        partialLabelScore ν left right R labels := by
…

Mentions: OAI.MaxCutGames.Repetition.rowSquareMass, OAI.MaxCutGames.Repetition.pairEnergy, OAI.MaxCutGames.Repetition.partialLabelScore

theorem OAI.MaxCutGames.Repetition.pairEnergy_le_of_labeling_gap line 88

Source documentation

A genuine gap for every deterministic labeling bounds the vector energy by an alphabet-independent quadratic gap.

theorem pairEnergy_le_of_labeling_gap (ν : FiniteDistribution E)
    (left right : E → V) (R : E → A → A → Bool)
    (a : V → Ω → A) (f : V → Ω → ℝ)
    (hf : ∀ v ω, 0 ≤ f v ω) (hrow : ∀ v, rowSquareMass f v ≤ 1)
    {g : ℝ} (hg : 0 < g)
    (hgap : ∀ labels : V → A, partialLabelScore ν left right R labels ≤ 1 - g) :
    pairEnergy ν left right R a f ≤ 1 - g ^ 2 / 8 := by
…

Mentions: OAI.MaxCutGames.Repetition.rowSquareMass, OAI.MaxCutGames.Repetition.partialLabelScore, OAI.MaxCutGames.Repetition.pairEnergy

def OAI.MaxCutGames.Repetition.rowMass line 127
Source documentation
The mass at each vertex, before or after determinization.
```
def rowMass (h : V → A → ℝ) (v : V) : ℝ := ∑ a, h v a
```
def OAI.MaxCutGames.Repetition.deterministicVector line 130
Source documentation
Move the full mass of each row to its selected label.
```
def deterministicVector [DecidableEq A] (h : V → A → ℝ) (labels : V → A)
    (v : V) (a : A) : ℝ :=
…
```
theorem OAI.MaxCutGames.Repetition.deterministicVector_rowMass line 135
theorem OAI.MaxCutGames.Repetition.rowMass_nonnegative line 141
theorem OAI.MaxCutGames.Repetition.deterministicVector_nonnegative line 146
theorem OAI.MaxCutGames.Repetition.deterministicVector_linear_image line 154
theorem OAI.MaxCutGames.Repetition.entry_eq_zero_of_rowMass_eq_zero line 161
def OAI.MaxCutGames.Repetition.rowLaw line 169
Source documentation
A zero row is harmless and uses a fixed fallback label.
```
def rowLaw [Nonempty A] (h : V → A → ℝ) (hh : ∀ v a, 0 ≤ h v a)
    (v : V) : FiniteDistribution A := by
…
```
theorem OAI.MaxCutGames.Repetition.rowLaw_expectation_mul_mass line 185

theorem OAI.MaxCutGames.Repetition.square_expectation_le line 199

Source documentation

Finite Jensen for the square, proved by expanding nonnegative variance.

theorem square_expectation_le {Ω : Type*} [Fintype Ω]
    (law : FiniteDistribution Ω) (f : Ω → ℝ) :
    law.expectation f ^ 2 ≤ law.expectation (fun x => f x ^ 2) := by
…

theorem OAI.MaxCutGames.Repetition.exists_expectation_le line 226
theorem OAI.MaxCutGames.Repetition.exists_deterministic_preserving_mass line 247
Source documentation
One label per vertex preserves every row's mass and can only improve the nonnegative weighted squared image under any fixed linear map. In particular, the same theorem applies separately at each coordinate of a vector-valued assignment; no product or independence property of those coordinates is used.
```
theorem exists_deterministic_preserving_mass [Nonempty A]
    (h : V → A → ℝ) (hh : ∀ v a, 0 ≤ h v a)
    (w : T → ℝ) (hw : ∀ t, 0 ≤ w t) (c : T → V → A → ℝ) :
    ∃ labels : V → A,
      (∑ t, w t * (∑ v, ∑ a, c t v a * h v a) ^ 2) ≤
        ∑ t, w t * (∑ v, c t v (labels v) * rowMass h v) ^ 2 := by
…
```
Mentions: OAI.MaxCutGames.Repetition.rowMass

theorem OAI.MaxCutGames.Repetition.exists_deterministic_vector line 295

Source documentation

The same conclusion stated directly as a deterministic nonnegative vector. Its row masses are exactly those of the original vector.

theorem exists_deterministic_vector [Nonempty A] [DecidableEq A]
    (h : V → A → ℝ) (hh : ∀ v a, 0 ≤ h v a)
    (w : T → ℝ) (hw : ∀ t, 0 ≤ w t) (c : T → V → A → ℝ) :
    ∃ labels : V → A,
      (∀ v a, 0 ≤ deterministicVector h labels v a) ∧
      (∀ v, rowMass (deterministicVector h labels) v = rowMass h v) ∧
      (∑ t, w t * (∑ v, ∑ a, c t v a * h v a) ^ 2) ≤
        ∑ t, w t * (∑ v, ∑ a, c t v a * deterministicVector h labels v a) ^ 2 := by
…

Mentions: OAI.MaxCutGames.Repetition.deterministicVector, OAI.MaxCutGames.Repetition.rowMass

structure OAI.MaxCutGames.Repetition.ProjectionKernel line 320
def OAI.MaxCutGames.Repetition.ProjectionKernel.toGame line 332
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.toGame_isProjection line 342
def OAI.MaxCutGames.Repetition.ProjectionKernel.apply line 346
Source documentation
Apply the projection operator to an arbitrary real assignment table.
```
def apply (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (f : Q₁ → A₁ → ℝ) (y : Q₂) (b : A₂) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel
def OAI.MaxCutGames.Repetition.ProjectionKernel.energy line 351
Source documentation
Squared Hilbert norm, with the actual right-question marginal.
```
def energy (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (f : Q₁ → A₁ → ℝ) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel
def OAI.MaxCutGames.Repetition.ProjectionKernel.assignment line 354
def OAI.MaxCutGames.Repetition.ProjectionKernel.assignmentEnergy line 358
def OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue line 362
Source documentation
Maximum squared collision norm of an ordinary deterministic left strategy.
```
def collisionValue [Nonempty A₁] (K : ProjectionKernel Q₁ Q₂ A₁ A₂) : ℝ := by
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel
def OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy line 366
def OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass line 369
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.energy_nonneg line 372
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.assignmentEnergy_le_collisionValue line 377
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_le_iff line 383
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.exists_optimal_assignment line 389
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.collisionValue_nonneg line 397
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_assignment line 403
abbrev OAI.MaxCutGames.Repetition.ProjectionKernel.SymmetricEdge line 448
def OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricLeft line 450
def OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricRight line 452
def OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricDistribution line 454
def OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricAccept line 478
def OAI.MaxCutGames.Repetition.ProjectionKernel.singleLabelVector line 485
Source documentation
A coordinate has one possible nonzero label at each question.
```
def singleLabelVector (a : Q₁ → Ω → A₁) (f : Q₁ → Ω → ℝ)
    (ω : Ω) (x : Q₁) (b : A₁) : ℝ := by
…
```
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.sum_projection_gates line 490
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_single_label line 520
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.energy_single_label line 540
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorEnergy_singleLabelVector line 583
Source documentation
Coordinate expansion and the symmetrized edge law agree exactly.
```
theorem vectorEnergy_singleLabelVector (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (a : Q₁ → Ω → A₁) (f : Q₁ → Ω → ℝ) :
    K.vectorEnergy (singleLabelVector a f) =
      pairEnergy K.symmetricDistribution symmetricLeft symmetricRight K.symmetricAccept a f := by
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.singleLabelVector, OAI.MaxCutGames.Repetition.pairEnergy, OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricLeft, OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricRight
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.symmetric_probability_eq_assignmentEnergy line 597
Source documentation
Ordinary deterministic labelings give the collision assignment energy.
```
theorem symmetric_probability_eq_assignmentEnergy (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (labels : Q₁ → A₁) :
    K.symmetricDistribution.probability (fun e =>
      K.symmetricAccept e (labels (symmetricLeft e)) (labels (symmetricRight e))) =
        K.assignmentEnergy labels := by
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricLeft, OAI.MaxCutGames.Repetition.ProjectionKernel.symmetricRight
def OAI.MaxCutGames.Repetition.ProjectionKernel.linearCoefficient line 625
Source documentation
Explicit matrix coefficients of the projection operator.
```
def linearCoefficient (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (t : Q₂ × A₂) (x : Q₁) (a : A₁) : ℝ :=
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.apply_eq_linearCoefficient_sum line 629
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.energy_eq_linearCoefficient_sum line 640
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.exists_energy_le_deterministicVector line 649
Source documentation
Scalar kernel determinization preserves the whole mass at every question.
```
theorem exists_energy_le_deterministicVector [Nonempty A₁]
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (h : Q₁ → A₁ → ℝ) (hh : ∀ x a, 0 ≤ h x a) :
    ∃ labels : Q₁ → A₁,
      K.energy h ≤ K.energy (deterministicVector h labels) := by
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.deterministicVector
def OAI.MaxCutGames.Repetition.ProjectionKernel.vectorAmplitude line 663
Source documentation
The amplitude at a question is the sum of its original label entries.
```
def vectorAmplitude (h : Ω → Q₁ → A₁ → ℝ) (x : Q₁) (ω : Ω) : ℝ :=
…
```
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.vectorAmplitude_nonnegative line 668
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.rowSquareMass_vectorAmplitude line 674
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.exists_vectorEnergy_le_singleLabelVector line 679
Source documentation
Auxiliary coordinates are determinized separately; they need not be independent, normalized, or nonempty.
```
theorem exists_vectorEnergy_le_singleLabelVector [Nonempty A₁]
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (h : Ω → Q₁ → A₁ → ℝ) (hh : ∀ ω x a, 0 ≤ h ω x a) :
    ∃ labels : Q₁ → Ω → A₁,
      K.vectorEnergy h ≤ K.vectorEnergy (singleLabelVector labels (vectorAmplitude h)) := by
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.ProjectionKernel.singleLabelVector, OAI.MaxCutGames.Repetition.ProjectionKernel.vectorAmplitude
theorem OAI.MaxCutGames.Repetition.ProjectionKernel.exists_mass_preserving_singleLabelVector line 702
Source documentation
Package the deterministic labels, amplitudes, exact mass preservation, and energy inequality for use by the finite threshold-rounding construction.
```
theorem exists_mass_preserving_singleLabelVector [Nonempty A₁]
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (h : Ω → Q₁ → A₁ → ℝ) (hh : ∀ ω x a, 0 ≤ h ω x a) :
    ∃ (labels : Q₁ → Ω → A₁) (f : Q₁ → Ω → ℝ),
      (∀ x ω, 0 ≤ f x ω) ∧
      (∀ x, rowSquareMass f x = vectorMass h x) ∧
      K.vectorEnergy h ≤ K.vectorEnergy (singleLabelVector labels f) := by
…
```
Mentions: OAI.MaxCutGames.Repetition.ProjectionKernel, OAI.MaxCutGames.Repetition.rowSquareMass, OAI.MaxCutGames.Repetition.ProjectionKernel.vectorMass, OAI.MaxCutGames.Repetition.ProjectionKernel.singleLabelVector