RoundingPaddingLemmas.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Finite vertex-specific padding of nonnegative vectors to unit squared row mass. The new coordinates can only increase any nonnegative relation energy.

def OAI.UniqueGamesTheorem.Repetition.rowSquareMass line 23
def OAI.UniqueGamesTheorem.Repetition.paddedAmplitude line 25
def OAI.UniqueGamesTheorem.Repetition.paddedLabel line 29
theorem OAI.UniqueGamesTheorem.Repetition.paddedAmplitude_nonnegative line 34
theorem OAI.UniqueGamesTheorem.Repetition.paddedAmplitude_row line 45
def OAI.UniqueGamesTheorem.Repetition.pairEnergy line 56
def OAI.UniqueGamesTheorem.Repetition.pairOverlap line 62
theorem OAI.UniqueGamesTheorem.Repetition.pairEnergy_nonnegative line 69
theorem OAI.UniqueGamesTheorem.Repetition.pairEnergy_le_padded line 81
theorem OAI.UniqueGamesTheorem.Repetition.pairQuadraticMass_eq_one line 128
theorem OAI.UniqueGamesTheorem.Repetition.pairGatedCorrelation_eq_energy line 150
theorem OAI.UniqueGamesTheorem.Repetition.pairGatedMinimum_eq_overlap line 160
theorem OAI.UniqueGamesTheorem.Repetition.pairEnergy_le_one_of_unit_rows line 170
theorem OAI.UniqueGamesTheorem.Repetition.pairOverlap_ge_energy line 183
Source documentation
The overlap used by finite threshold sampling is large whenever the actual weighted occurrence energy is large.
```
theorem pairOverlap_ge_energy (ν : 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) :
    1 - Real.sqrt (2 * (1 - pairEnergy ν left right R a f)) ≤
      pairOverlap ν left right R a f := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.rowSquareMass, OAI.UniqueGamesTheorem.Repetition.pairEnergy, OAI.UniqueGamesTheorem.Repetition.pairOverlap
abbrev OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.SymmetricEdge line 222
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricLeft line 224
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricRight line 226
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricDistribution line 228
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricAccept line 252
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.singleLabelVector line 259
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.UniqueGamesTheorem.Repetition.ProjectionKernel.sum_projection_gates line 264
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_single_label line 294
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy_single_label line 314
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy_singleLabelVector line 357
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.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.singleLabelVector, OAI.UniqueGamesTheorem.Repetition.pairEnergy, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricLeft, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricRight
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetric_probability_eq_assignmentEnergy line 371
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.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricLeft, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.symmetricRight
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.linearCoefficient line 408
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.UniqueGamesTheorem.Repetition.ProjectionKernel
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_eq_linearCoefficient_sum line 412
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy_eq_linearCoefficient_sum line 423
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.exists_energy_le_deterministicVector line 432
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.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.deterministicVector
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorAmplitude line 446
Source documentation
The amplitude at a question is the sum of its original label entries.
```
def vectorAmplitude (h : Ω → Q₁ → A₁ → ℝ) (x : Q₁) (ω : Ω) : ℝ :=
…
```
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorAmplitude_nonnegative line 450
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.rowSquareMass_vectorAmplitude line 456
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.exists_vectorEnergy_le_singleLabelVector line 461
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.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.singleLabelVector, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorAmplitude
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.exists_mass_preserving_singleLabelVector line 484
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.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.rowSquareMass, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.singleLabelVector