TensorAlgebraLemmas.lean`

42 declarations, 0 contain sorry, 0 declared as axioms

Finite-sum tensor factorization used by projection-game collision operators. No restriction to coordinatewise strategies occurs: f below is an arbitrary function of both input questions and both input answers.

def OAI.UniqueGamesTheorem.Repetition.kernelApply line 35
Source documentation
Apply a finite real kernel. Output indices need no finiteness assumption.
```
def kernelApply (K : Y → B → X → A → ℝ) (f : X → A → ℝ) (y : Y) (b : B) : ℝ :=
…
```

def OAI.UniqueGamesTheorem.Repetition.tensorKernel line 39

Source documentation

Independent tensor of two kernels.

def tensorKernel (K : Y → B → X → A → ℝ) (L : Z → C → U → D → ℝ)
    (yz : Y × Z) (bc : B × C) (xu : X × U) (ad : A × D) : ℝ :=
…

theorem OAI.UniqueGamesTheorem.Repetition.kernelApply_tensor line 45
Source documentation
Applying the tensor first applies L separately for every fixed input of K, and then applies K. This is valid for arbitrary coupled inputs.
```
theorem kernelApply_tensor
    (K : Y → B → X → A → ℝ) (L : Z → C → U → D → ℝ)
    (f : (X × U) → (A × D) → ℝ) (y : Y) (z : Z) (b : B) (c : C) :
    kernelApply (tensorKernel K L) f (y,z) (b,c) =
      kernelApply K (fun x a => kernelApply L (fun u d => f (x,u) (a,d)) z c) y b := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.kernelApply, OAI.UniqueGamesTheorem.Repetition.tensorKernel
theorem OAI.UniqueGamesTheorem.Repetition.kernelApply_nonnegative line 59
theorem OAI.UniqueGamesTheorem.Repetition.kernelApply_sum line 70
Source documentation
Summing a family of input functions commutes with the finite operator.
```
theorem kernelApply_sum
    (K : Y → B → X → A → ℝ) (f : I → X → A → ℝ) (y : Y) (b : B) :
    kernelApply K (fun x a => ∑ i, f i x a) y b =
      ∑ i, kernelApply K (f i) y b := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.kernelApply
theorem OAI.UniqueGamesTheorem.Repetition.kernelApply_smul line 84
theorem OAI.UniqueGamesTheorem.Repetition.kernelApply_slice_mass line 97
Source documentation
Marginalizing the first answer of a joint input strategy after applying the second kernel is the same as applying the kernel to the answer marginal.
```
theorem kernelApply_slice_mass
    (L : Z → C → U → D → ℝ) (f : (X × U) → (A × D) → ℝ)
    (x : X) (z : Z) (c : C) :
    (∑ a, kernelApply L (fun u d => f (x,u) (a,d)) z c) =
      kernelApply L (fun u d => ∑ a, f (x,u) (a,d)) z c := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.kernelApply
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.coefficients line 126
Source documentation
The coefficient form of the conditional projection operator.
```
def coefficients (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (y : Q₂) (b : A₂) (x : Q₁) (a : A₁) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_eq_kernelApply line 130
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_nonnegative line 142
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_sum line 154
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_smul line 160
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.product line 167
Source documentation
Independent product of the outer and conditional laws.
```
def product (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂) :
    ProjectionKernel (Q₁ × R₁) (Q₂ × R₂) (A₁ × B₁) (A₂ × B₂) where
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.coefficients_product line 179

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply_product line 188

Source documentation

Arbitrary product inputs factor through the second game operator.

theorem apply_product (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (f : (Q₁ × R₁) → (A₁ × B₁) → ℝ)
    (y : Q₂) (z : R₂) (b : A₂) (c : B₂) :
    (K.product H).apply f (y,z) (b,c) =
      K.apply (fun x a => H.apply (fun u d => f (x,u) (a,d)) z c) y b := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.apply

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.toGame_product line 199
Source documentation
The kernel tensor realizes the ordinary independent conjunction game.
```
theorem toGame_product (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂) :
    (K.product H).toGame = UniqueGamesTheorem.Repetition.product K.toGame H.toGame := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.toGame, OAI.UniqueGamesTheorem.Repetition.product
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.repetition line 243
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.repetition_accepts_iff line 256
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.toGame_repetition line 263
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.eq_of_data_eq line 281

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.repetition_succ line 293

Source documentation

Separate the first coordinate without restricting answer dependence on any coordinate of the complete local question tuple.

theorem repetition_succ (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (n : Nat) :
    K.repetition (n + 1) =
      (K.product (K.repetition n)).reindex
        (Fin.consEquiv (fun _ : Fin (n + 1) => Q₁))
        (Fin.consEquiv (fun _ : Fin (n + 1) => Q₂))
        (Fin.consEquiv (fun _ : Fin (n + 1) => A₁))
        (Fin.consEquiv (fun _ : Fin (n + 1) => A₂)) := by
…

Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.reindex

theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_repetition_succ line 326
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_repetition_zero_le_one line 332
def OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.tensorSlice line 364
Source documentation
Apply the second game to a fixed first question and first answer. The square-root factor changes its weighted output space into counting measure.
```
def tensorSlice (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (labels : (Q₁ × R₁) → (A₁ × B₁))
    (ω : R₂ × B₂) (x : Q₁) (a : A₁) : ℝ :=
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.tensorSlice_nonnegative line 371
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.sum_assignment_product line 385
Source documentation
Marginalizing the first label of a deterministic product strategy leaves the deterministic second-label strategy.
```
theorem sum_assignment_product (labels : (Q₁ × R₁) → (A₁ × B₁))
    (x : Q₁) (u : R₁) (d : B₁) :
    (∑ a, assignment labels (x,u) (a,d)) =
      assignment (fun r => (labels (x,r)).2) u d := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignment
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.tensorSlice_label_mass line 393
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass_tensorSlice line 405
Source documentation
The fiber mass is an actual collision energy of the second game, not a free normalization assumption.
```
theorem vectorMass_tensorSlice (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (labels : (Q₁ × R₁) → (A₁ × B₁)) (x : Q₁) :
    vectorMass (H.tensorSlice labels) x =
      H.assignmentEnergy (fun r => (labels (x,r)).2) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass_tensorSlice_le line 418
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy_tensorSlice line 426
Source documentation
Exact Hilbert-norm factorization, with every marginal weight retained.
```
theorem vectorEnergy_tensorSlice (K : ProjectionKernel Q₁ Q₂ A₁ A₂)
    (H : ProjectionKernel R₁ R₂ B₁ B₂)
    (labels : (Q₁ × R₁) → (A₁ × B₁)) :
    K.vectorEnergy (H.tensorSlice labels) = (K.product H).assignmentEnergy labels := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.assignmentEnergy
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass_smul line 496
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.energy_smul line 502
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy_smul line 513
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.entry_eq_zero_of_vectorMass_nonpositive line 521
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy_eq_zero_of_mass_nonpositive line 535
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorEnergy_le_of_unit_bound line 548
Source documentation
A unit-mass estimate extends to any nonnegative mass bound, including zero. The hypothesis is precisely the unit-mass analytic estimate being normalized; the normalization itself assumes no repetition bound.
```
theorem vectorEnergy_le_of_unit_bound
    (K : ProjectionKernel Q₁ Q₂ A₁ A₂) (ρ C : ℝ)
    (unit_bound : ∀ f : Ω → Q₁ → A₁ → ℝ,
      (∀ ω x a, 0 ≤ f ω x a) → (∀ x, vectorMass f x ≤ 1) → K.vectorEnergy f ≤ ρ)
    (hC : 0 ≤ C) (f : Ω → Q₁ → A₁ → ℝ)
    (hf : ∀ ω x a, 0 ≤ f ω x a) (hmass : ∀ x, vectorMass f x ≤ C) :
    K.vectorEnergy f ≤ ρ * C := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.ProjectionKernel, OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.vectorMass
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.collisionValue_product_le_gap_rate line 606
theorem OAI.UniqueGamesTheorem.Repetition.ProjectionKernel.repetition_value_le_dsRate line 620
theorem OAI.UniqueGamesTheorem.Repetition.projection_repetition_value line 645
Source documentation
The v2 projection-repetition estimate, including the empty product. The repetition exponent is independent of all question and answer cardinalities.
```
theorem projection_repetition_value
    (G : Game Q₁ Q₂ A₁ A₂) (hG : IsProjection G) (n : ℕ)
    {gap : ℝ} (hgap₀ : 0 < gap) (hgap₁ : gap < 1)
    (hvalue : G.value ≤ 1 - gap) :
    (G.repetition n).value ≤ (1 - gap ^ 2 / 16) ^ n := by
…
```
Mentions: OAI.UniqueGamesTheorem.Repetition.IsProjection
theorem OAI.UniqueGamesTheorem.Repetition.projection_repetition_success line 654
theorem OAI.UniqueGamesTheorem.Repetition.clean_repetition_value line 663
theorem OAI.UniqueGamesTheorem.Repetition.final_repetition_value line 675