noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAcceptSet {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) : Finset (Fin L)

Equations

• QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAcceptSet accepted history = {j : Fin L | accepted j (history j.castSucc)}

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) : Fin (L + 1)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_prefix_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) (j : Fin L) : dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = j.succ ↔ accepted j (history j.castSucc) ∧ ∀ i < j, ¬accepted i (history i.castSucc)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_zero_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) : dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = 0 ↔ ∀ (i : Fin L), ¬accepted i (history i.castSucc)

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptEquiv {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) : Equiv.Perm ((_ : Fin (L + 1)) × (Fin (L + 1) → β))

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) : ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × (Fin (L + 1) → β)) ℂ)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary_mulVec {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (v : (_ : Fin (L + 1)) × (Fin (L + 1) → β) → ℂ) (flag : Fin (L + 1)) (history : Fin (L + 1) → β) : (↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted)).mulVec v ⟨flag, history⟩ = v ⟨(Equiv.swap 0 (dSVDensityRationalHeterogeneousActualFirstAccepted accepted history)) flag, history⟩

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAcceptUnitary_zeroFlag {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (v : (Fin (L + 1) → β) → ℂ) (flag : Fin (L + 1)) (history : Fin (L + 1) → β) : (↑(dSVDensityRationalHeterogeneousActualFirstAcceptUnitary accepted)).mulVec (fun (q : (_ : Fin (L + 1)) × (Fin (L + 1) → β)) => if q.fst = 0 then v q.snd else 0) ⟨flag, history⟩ = if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then v history else 0

def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCopyAccepted {S N d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (j : Fin L) (atom : DSVUniformDensityThresholdLocalIndex N d) : Prop

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualCopyCondition {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (flag i : Fin (L + 1)) (atom : β) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_allFlags_iff {β : Type u_1} {L : ℕ} (accepted : Fin L → β → Prop) (history : Fin (L + 1) → β) (flag : Fin (L + 1)) : dSVDensityRationalHeterogeneousActualFirstAccepted accepted history = flag ↔ ∀ (i : Fin (L + 1)), dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i (history i)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualFirstAccepted_sourceProduct {β : Type u_1} [Fintype β] {L : ℕ} (accepted : Fin L → β → Prop) (flag : Fin (L + 1)) (A D : Fin (L + 1) → β → ℂ) : (∑ history : Fin (L + 1) → β, (∏ i : Fin (L + 1), A i (history i)) * if flag = dSVDensityRationalHeterogeneousActualFirstAccepted accepted history then ∏ i : Fin (L + 1), D i (history i) else 0) = ∏ i : Fin (L + 1), ∑ atom : β, A i atom * if dSVDensityRationalHeterogeneousActualCopyCondition accepted flag i atom then D i atom else 0

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalLocalUnitary {β : Type u_1} [Fintype β] [DecidableEq β] {L : ℕ} (accepted : Fin L → β → Prop) (U : ↥(Matrix.unitaryGroup β ℂ)) : ↥(Matrix.unitaryGroup ((_ : Fin (L + 1)) × (Fin (L + 1) → β)) ℂ)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualAliceUnitary (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualBobUnitary (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ζ : BipartiteUnitVector d) : ↥(Matrix.unitaryGroup (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L) ℂ)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState (N : ℕ) {S d L : ℕ} (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : EuclideanSpace ℂ (DSVUniformDensityThresholdWholeHistoryLocalIndex N d L × DSVUniformDensityThresholdWholeHistoryLocalIndex N d L)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousActualPhysicalState_norm {S N d L : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ‖dSVDensityRationalHeterogeneousActualPhysicalState N width schedule ξ ζ‖ = 1

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageOutcome {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) (alice bob : Bool) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageContinue {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageSuccess {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageOutcome_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) (alice bob : Bool) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalStageOutcome N width schedule ξ ζ k alice bob

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStage_partition {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k = 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_eq_hazard {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k = dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ℝ

Equations

• QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ = QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ L

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStopped_mass_partition {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedSuccessMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ + dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ = 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_eq_hazard {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ = ∑ k : Fin L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ ↑k * dSVDensityRationalPhysicalProjectorCrossHazard N (width (schedule k)) ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_nonneg {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : 0 ≤ dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageHazardRatio {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_eq_escape_mul_ratio {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : ℕ) : dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k = (dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k) * dSVDensityRationalHeterogeneousPhysicalStageHazardRatio N width schedule ξ ζ k

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_eq_ratioLedger {d S L : ℕ} (N : ℕ) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ = ∑ k ∈ Finset.range L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k * (dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k) * dSVDensityRationalHeterogeneousPhysicalStageHazardRatio N width schedule ξ ζ k

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_lower {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (k : Fin L) : 1 / (2 * (width (schedule k) + 1) * ↑d) ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStage_escape_ge_diagonal {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ ↑k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageAsynchronous_relative_diagonal_le {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k / dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (width (schedule k) + 1) * (↑d / ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageHazardRatio_le_relative_diagonal {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageHazardRatio N width schedule ξ ζ ↑k ≤ dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ ↑k / dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageHazardRatio_le_targetDistance {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageHazardRatio N width schedule ξ ζ ↑k ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (W + 1) * (↑d / ↑N)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedEscape_budget {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : ∑ k ∈ Finset.range L, dSVDensityRationalHeterogeneousPhysicalSurvival N width schedule ξ ζ k * (dSVDensityRationalHeterogeneousPhysicalStageSuccess N width schedule ξ ζ k + dSVDensityRationalHeterogeneousPhysicalStageAsynchronous N width schedule ξ ζ k) ≤ 1

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass_le_targetDistance {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (upper : ∀ (s : Fin S), width s ≤ W) (W_nonnegative : 0 ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalStoppedAsynchronousMass N width schedule ξ ζ ≤ 8 * √2 * ‖↑ξ - ↑ζ‖ + 2 * (W + 1) * (↑d / ↑N)

noncomputable def QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate (d : ℕ) (W : ℝ) : ℝ

Equations

• QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W = 1 / (2 * (W + 1) * ↑d)

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate_pos {d : ℕ} (dimension : 0 < d) {W : ℝ} (W_nonnegative : 0 ≤ W) : 0 < dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate_le_half {d : ℕ} (dimension : 0 < d) {W : ℝ} (W_nonnegative : 0 ≤ W) : dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W ≤ 1 / 2

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageDiagonalSuccess_ge_uniform {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W ≤ dSVDensityRationalPhysicalDiagonalBornSuccess grid dimension (width (schedule k)) ξ

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalStageContinue_le_uniform {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) (k : Fin L) : dSVDensityRationalHeterogeneousPhysicalStageContinue N width schedule ξ ζ ↑k ≤ 1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_le_pow {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ ≤ (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysical_exists_positive_horizon {d : ℕ} (dimension : 0 < d) {W ε : ℝ} (W_nonnegative : 0 ≤ W) (precision : 0 < ε) : ∃ (L : ℕ), 0 < L ∧ (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L ≤ ε ^ 2

theorem QuantumParallelRepetition.dSVDensityRationalHeterogeneousPhysicalTerminalMass_le_horizon {d S L N : ℕ} (grid : 0 < N) (dimension : 0 < d) (width : Fin S → ℝ) (large : ∀ (s : Fin S), 1 ≤ width s) (fine : ∀ (s : Fin S), ↑d / ↑N ≤ 1 / (2 * (width s + 1))) {W ε : ℝ} (W_nonnegative : 0 ≤ W) (upper : ∀ (s : Fin S), width s ≤ W) (tail : (1 - dSVDensityRationalHeterogeneousPhysicalUniformEscapeRate d W) ^ L ≤ ε ^ 2) (schedule : Fin L → Fin S) (ξ ζ : BipartiteUnitVector d) : dSVDensityRationalHeterogeneousPhysicalTerminalMass N width schedule ξ ζ ≤ ε ^ 2

noncomputable def QuantumParallelRepetition.fairPartitionWeight (α : Type u_2) [Fintype α] : ℝ

Equations

• QuantumParallelRepetition.fairPartitionWeight α = (2 ^ Fintype.card α)⁻¹

noncomputable def QuantumParallelRepetition.reversePartitionWeight {α : Type u_1} [Fintype α] (s : Finset α) : ℝ

Equations

• QuantumParallelRepetition.reversePartitionWeight s = QuantumParallelRepetition.fairPartitionWeight α * (2 * ↑s.card / ↑(Fintype.card α))

noncomputable def QuantumParallelRepetition.forwardMarkedPartitionWeight (α : Type u_2) [Fintype α] : ℝ

Equations

• QuantumParallelRepetition.forwardMarkedPartitionWeight α = 2 * QuantumParallelRepetition.fairPartitionWeight α / ↑(Fintype.card α)

noncomputable def QuantumParallelRepetition.reverseMarkedPartitionWeight {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (i : α) : ℝ

Equations

• QuantumParallelRepetition.reverseMarkedPartitionWeight s i = if i ∈ s then QuantumParallelRepetition.reversePartitionWeight s / ↑s.card else 0

theorem QuantumParallelRepetition.fairPartitionWeight_pos {α : Type u_1} [Fintype α] : 0 < fairPartitionWeight α

theorem QuantumParallelRepetition.fairPartitionWeight_nonneg {α : Type u_1} [Fintype α] : 0 ≤ fairPartitionWeight α

theorem QuantumParallelRepetition.fairPartitionWeight_sum {α : Type u_1} [Fintype α] : ∑ _s : Finset α, fairPartitionWeight α = 1

theorem QuantumParallelRepetition.reversePartitionWeight_nonneg {α : Type u_1} [Fintype α] (s : Finset α) : 0 ≤ reversePartitionWeight s

@[simp]

theorem QuantumParallelRepetition.reversePartitionWeight_empty {α : Type u_1} [Fintype α] : reversePartitionWeight ∅ = 0

theorem QuantumParallelRepetition.reversePartitionWeight_pos_iff {α : Type u_1} [Fintype α] (hα : 0 < Fintype.card α) (s : Finset α) : 0 < reversePartitionWeight s ↔ s.Nonempty

theorem QuantumParallelRepetition.reverseMarkedPartitionWeight_eq_forward {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {i : α} (hi : i ∈ s) : reverseMarkedPartitionWeight s i = forwardMarkedPartitionWeight α

noncomputable def QuantumParallelRepetition.rightSpectralBornWeight {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (i : dB) : ℝ

Equations

• QuantumParallelRepetition.rightSpectralBornWeight ρ F G hG i = ((QuantumParallelRepetition.bornTracePairing ρ.matrix) F) (QuantumParallelRepetition.positiveMatrixSpectralAtom G hG i)

theorem QuantumParallelRepetition.rightSpectralBornWeight_nonneg {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (i : dB) : 0 ≤ rightSpectralBornWeight ρ F G hG i

theorem QuantumParallelRepetition.rightSpectralBornWeight_sum {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) : ∑ i : dB, rightSpectralBornWeight ρ F G hG i = ((bornTracePairing ρ.matrix) F) 1

theorem QuantumParallelRepetition.rightSpectralBornWeight_moment {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) : ∑ i : dB, rightSpectralBornWeight ρ F G hG i * ⋯.eigenvalues i = ((bornTracePairing ρ.matrix) F) G

theorem QuantumParallelRepetition.rightSpectralBornWeight_entropy {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) : ((bornTracePairing ρ.matrix) F) (cfc (fun (z : ℝ) => z * Real.log z) G) = ∑ i : dB, rightSpectralBornWeight ρ F G hG i * (⋯.eigenvalues i * Real.log (⋯.eigenvalues i))

theorem QuantumParallelRepetition.rightSpectralBornWeight_negEntropy {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) : -((bornTracePairing ρ.matrix) F) (cfc (fun (z : ℝ) => z * Real.log z) G) = ∑ i : dB, rightSpectralBornWeight ρ F G hG i * (⋯.eigenvalues i).negMulLog

theorem QuantumParallelRepetition.bornTracePairing_le_one_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hFcomplement : (1 - F).PosSemidef) : ((bornTracePairing ρ.matrix) F) 1 ≤ 1

theorem QuantumParallelRepetition.matrixLogEntropy_born_lower_bound_right {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : -((bornTracePairing ρ.matrix) F) (cfc (fun (z : ℝ) => z * Real.log z) G) ≤ (((bornTracePairing ρ.matrix) F) G).negMulLog

def QuantumParallelRepetition.fullSubsetHistoryFieldEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) : FullSubsetHistory X Y n D L ≃ (↥D → X × Y) × (↥L → X) × (↥(fullHistoryRemaining n D L) → Y)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullHistoryWeight_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) : ∑ h : FullSubsetHistory X Y n D L, fullHistoryWeight G h = 1

theorem QuantumParallelRepetition.fullHistoryWinIndicator_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {D L : Finset (Fin n)} (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G h α β ≤ 1

def QuantumParallelRepetition.fullHistoryAnswerCount {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ℝ

Equations

• QuantumParallelRepetition.fullHistoryAnswerCount D = ↑(Fintype.card (↥D → A)) * ↑(Fintype.card (↥D → B))

theorem QuantumParallelRepetition.fullHistoryAnswerCount_eq {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : fullHistoryAnswerCount D = ↑(Fintype.card A) ^ D.card * ↑(Fintype.card B) ^ D.card

@[reducible, inline]

abbrev QuantumParallelRepetition.FullHistoryEntropyAtom (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (n : ℕ) (D L : Finset (Fin n)) : Type (max (max u_6 u_5) u_8 u_7)

Equations

• QuantumParallelRepetition.FullHistoryEntropyAtom X Y A B n D L = (QuantumParallelRepetition.FullSubsetHistory X Y n D L × (↥D → A) × (↥D → B))

def QuantumParallelRepetition.fullHistoryAtomCountingWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : ℝ

Equations

• QuantumParallelRepetition.fullHistoryAtomCountingWeight G D L t = QuantumParallelRepetition.fullHistoryWeight G t.1 * QuantumParallelRepetition.fullHistoryWinIndicator G t.1 t.2.1 t.2.2

noncomputable def QuantumParallelRepetition.fullHistoryAtomBornMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullHistoryAtomCountingWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : 0 ≤ fullHistoryAtomCountingWeight G D L t

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : 0 ≤ fullHistoryAtomBornMass G n S D L t

theorem QuantumParallelRepetition.bornTracePairing_contractions_le_one {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : ((bornTracePairing ρ.matrix) F) G ≤ 1

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (t : FullHistoryEntropyAtom X Y A B n D L) : fullHistoryAtomBornMass G n S D L t ≤ 1

theorem QuantumParallelRepetition.fullHistoryAtomCountingWeight_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) : ∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t ≤ fullHistoryAnswerCount D

theorem QuantumParallelRepetition.fullHistoryAtomBornMass_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) : ∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t * fullHistoryAtomBornMass G n S D L t = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)

theorem QuantumParallelRepetition.fullHistoryAtomEntropy_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) : ∑ t : FullHistoryEntropyAtom X Y A B n D L, fullHistoryAtomCountingWeight G D L t * (fullHistoryAtomBornMass G n S D L t).negMulLog ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_lower_bound {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (hL : L ⊆ Finset.univ \ D) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) : -((strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))) ≤ fullHistoryAliceEntropyPotential G n S D L

structure QuantumParallelRepetition.FullCoordinateRevealHistory (X : Type u_1) (Y : Type u_2) [Fintype X] [Fintype Y] (n : ℕ) (D L : Finset (Fin n)) (i : Fin n) : Type (max u_1 u_2)

• aliceConditioned : ↥D → X
• bobConditioned : ↥D → Y
• aliceRevealed : ↥L → X
• bobRemaining : ↥(fullHistoryRemaining n D (insert i L)) → Y

theorem QuantumParallelRepetition.FullCoordinateRevealHistory.ext {X : Type u_1} {Y : Type u_2} {inst✝ : Fintype X} {inst✝¹ : Fintype Y} {n : ℕ} {D L : Finset (Fin n)} {i : Fin n} {x y : FullCoordinateRevealHistory X Y n D L i} (aliceConditioned : x.aliceConditioned = y.aliceConditioned) (bobConditioned : x.bobConditioned = y.bobConditioned) (aliceRevealed : x.aliceRevealed = y.aliceRevealed) (bobRemaining : x.bobRemaining = y.bobRemaining) : x = y

@[instance_reducible]

instance QuantumParallelRepetition.instFintypeFullCoordinateRevealHistory {X✝ : Type u_1} {Y✝ : Type u_2} {inst✝ : Fintype X✝} {inst✝¹ : Fintype Y✝} {n✝ : ℕ} {D✝ L✝ : Finset (Fin n✝)} {i✝ : Fin n✝} [Fintype X✝] [Fintype Y✝] : Fintype (FullCoordinateRevealHistory X✝ Y✝ n✝ D✝ L✝ i✝)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullHistoryRemaining_insert_subset {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) : fullHistoryRemaining n D (insert i L) ⊆ fullHistoryRemaining n D L

def QuantumParallelRepetition.fullCoordinateBaseOfOldHistory {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullSubsetHistory X Y n D L) : FullCoordinateRevealHistory X Y n D L i

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateOldHistory {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) (y : Y) : FullSubsetHistory X Y n D L

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateBaseOfNewHistory {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullSubsetHistory X Y n D (insert i L)) : FullCoordinateRevealHistory X Y n D L i

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateNewHistory {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) (x : X) : FullSubsetHistory X Y n D (insert i L)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateOldHistoryEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : FullSubsetHistory X Y n D L ≃ FullCoordinateRevealHistory X Y n D L i × Y

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateNewHistoryEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) : FullSubsetHistory X Y n D (insert i L) ≃ FullCoordinateRevealHistory X Y n D L i × X

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.finsetSubtype_prod_insert {ι : Type u_1} {T : Type u_2} [DecidableEq ι] [CommMonoid T] (s : Finset ι) (i : ι) (hi : i ∉ s) (f : ↥(insert i s) → T) : ∏ j : ↥(insert i s), f j = f ⟨i, ⋯⟩ * ∏ j : ↥s, f ⟨↑j, ⋯⟩

def QuantumParallelRepetition.fullHistoryRemainingCoordinateEquiv {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : ↥(fullHistoryRemaining n D L) ≃ Option ↥(fullHistoryRemaining n D (insert i L))

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullHistoryRemaining_prod_split {n : ℕ} {T : Type u_1} [CommMonoid T] (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (f : ↥(fullHistoryRemaining n D L) → T) : ∏ j : ↥(fullHistoryRemaining n D L), f j = f ⟨i, ⋯⟩ * ∏ j : ↥(fullHistoryRemaining n D (insert i L)), f ⟨↑j, ⋯⟩

def QuantumParallelRepetition.fullCoordinateBaseWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullCoordinateBaseWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullCoordinateRevealHistory X Y n D L i) : 0 ≤ fullCoordinateBaseWeight G D L i h

theorem QuantumParallelRepetition.fullCoordinateOldHistory_weight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (h : FullCoordinateRevealHistory X Y n D L i) (y : Y) : fullHistoryWeight G (fullCoordinateOldHistory D L i h y) = fullCoordinateBaseWeight G D L i h * G.marginalY y

theorem QuantumParallelRepetition.fullCoordinateNewHistory_weight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (h : FullCoordinateRevealHistory X Y n D L i) (x : X) : fullHistoryWeight G (fullCoordinateNewHistory D L i h x) = fullCoordinateBaseWeight G D L i h * G.marginalX x

theorem QuantumParallelRepetition.finitePurificationMatrix_pair_difference_gram_apply {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a b : ι) (i j : d) : ((finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b).conjTranspose * (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b)) i j = ∑ r : d, inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - ensemblePurificationSubspaceEntry F M positive hM b r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - ensemblePurificationSubspaceEntry F M positive hM b r j)

theorem QuantumParallelRepetition.ensemblePurificationSubspaceEntry_pair_difference_inner_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a b : ι) (r i j : d) : inner ℂ (ensemblePurificationSubspaceEntry F M positive hM a r i - ensemblePurificationSubspaceEntry F M positive hM b r i) (ensemblePurificationSubspaceEntry F M positive hM a r j - ensemblePurificationSubspaceEntry F M positive hM b r j) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s r i - spectralPurificationFilter (F b) ⋯ s r i) * (spectralPurificationFilter (F a) ⋯ s r j - spectralPurificationFilter (F b) ⋯ s r j)

theorem QuantumParallelRepetition.finitePurificationMatrix_pair_difference_gram_eq_integral {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (positive : ∀ (i : ι), (F i).PosSemidef) (hM : M.PosSemidef) (a b : ι) : (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b).conjTranspose * (finitePurificationMatrix F M positive hM a - finitePurificationMatrix F M positive hM b) = ∫ (s : ℝ) in Set.Ioi 0, star (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter (F b) ⋯ s) * (spectralPurificationFilter (F a) ⋯ s - spectralPurificationFilter (F b) ⋯ s)

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_left {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA KA' : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA' KB = finiteLocalPurificationVector S (KA - KA') KB

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB KB' : Matrix eB S.Bob ℂ) : finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA KB' = finiteLocalPurificationVector S KA (KB - KB')

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_left_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA KA' : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) : ‖finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA' KB‖ ^ 2 = ((bornTracePairing S.state.matrix) ((KA - KA').conjTranspose * (KA - KA'))) (KB.conjTranspose * KB)

theorem QuantumParallelRepetition.finiteLocalPurificationVector_sub_right_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB KB' : Matrix eB S.Bob ℂ) : ‖finiteLocalPurificationVector S KA KB - finiteLocalPurificationVector S KA KB'‖ ^ 2 = ((bornTracePairing S.state.matrix) (KA.conjTranspose * KA)) ((KB - KB').conjTranspose * (KB - KB'))

noncomputable def QuantumParallelRepetition.fullCoordinateAliceQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (x : X) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.fullCoordinateAliceMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (y : Y) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.fullCoordinateBobQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (β : ↥D → B) (y : Y) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.fullCoordinateBobMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (β : ↥D → B) (x : X) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateAssembleHiddenAlice {X : Type u_1} {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (x : X) (hidden : ↥(fullHistoryRemaining n D (insert i L)) → X) : ↥(fullHistoryRemaining n D L) → X

Equations

• QuantumParallelRepetition.fullCoordinateAssembleHiddenAlice D L i x hidden j = if hj : ↑j = i then x else hidden ⟨↑j, ⋯⟩

def QuantumParallelRepetition.fullCoordinateHiddenAliceEquiv {X : Type u_1} [Fintype X] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : (↥(fullHistoryRemaining n D L) → X) ≃ X × (↥(fullHistoryRemaining n D (insert i L)) → X)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateAssembleHiddenBob {Y : Type u_1} {n : ℕ} (L : Finset (Fin n)) (i : Fin n) (y : Y) (hidden : ↥L → Y) : ↥(insert i L) → Y

Equations

• QuantumParallelRepetition.fullCoordinateAssembleHiddenBob L i y hidden j = if hj : ↑j = i then y else hidden ⟨↑j, ⋯⟩

def QuantumParallelRepetition.fullCoordinateHiddenBobEquiv {Y : Type u_1} [Fintype Y] {n : ℕ} (L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) : (↥(insert i L) → Y) ≃ Y × (↥L → Y)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullCoordinateAliceQuestion_eq {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥(fullHistoryRemaining n D (insert i L)) → X) : fullHistoryAliceQuestion (fullCoordinateOldHistory D L i r y) (fullCoordinateAssembleHiddenAlice D L i x hidden) = fullHistoryAliceQuestion (fullCoordinateNewHistory D L i r x) hidden

theorem QuantumParallelRepetition.fullCoordinateBobQuestion_eq {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥L → Y) : fullHistoryBobQuestion (fullCoordinateNewHistory D L i r x) (fullCoordinateAssembleHiddenBob L i y hidden) = fullHistoryBobQuestion (fullCoordinateOldHistory D L i r y) hidden

theorem QuantumParallelRepetition.fullCoordinateHiddenAliceWeight_split {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥(fullHistoryRemaining n D (insert i L)) → X) : fullHistoryHiddenAliceWeight G (fullCoordinateOldHistory D L i r y) (fullCoordinateAssembleHiddenAlice D L i x hidden) = G.conditionalXGivenY y x * fullHistoryHiddenAliceWeight G (fullCoordinateNewHistory D L i r x) hidden

theorem QuantumParallelRepetition.fullCoordinateHiddenBobWeight_split {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥L → Y) : fullHistoryHiddenBobWeight G (fullCoordinateNewHistory D L i r x) (fullCoordinateAssembleHiddenBob L i y hidden) = G.conditionalYGivenX x y * fullHistoryHiddenBobWeight G (fullCoordinateOldHistory D L i r y) hidden

theorem QuantumParallelRepetition.fullCoordinateAliceFilter_conditional_mean {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (y : Y) : fullCoordinateAliceMeanFilter G n S D L i r α y = conditionalAliceAverage G (fullCoordinateAliceQuestionFilter G n S D L i r α) y

theorem QuantumParallelRepetition.fullCoordinateBobFilter_conditional_mean {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (β : ↥D → B) (x : X) : fullCoordinateBobMeanFilter G n S D L i r β x = conditionalBobAverage G (fullCoordinateBobQuestionFilter G n S D L i r β) x

theorem QuantumParallelRepetition.matrixLogEntropy_weighted_jensen_posSemidef {ι : Type u_1} {d : Type u_2} [Fintype ι] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : ι → Matrix d d ℂ) (M : Matrix d d ℂ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (mean : ∑ i : ι, weight i • F i = M) (positive : ∀ (i : ι), (F i).PosSemidef) : (∑ i : ι, weight i • cfc (fun (z : ℝ) => z * Real.log z) (F i) - cfc (fun (z : ℝ) => z * Real.log z) M).PosSemidef

theorem QuantumParallelRepetition.conditionalAlice_matrixLogEntropy_gap_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {d : Type u_5} [Fintype d] [DecidableEq d] (G : Game X Y A B) (H : X → Matrix d d ℂ) (hH : ∀ (x : X), (H x).PosSemidef) (y : Y) (hy : 0 < G.marginalY y) : (conditionalAliceAverage G (fun (x : X) => cfc (fun (z : ℝ) => z * Real.log z) (H x)) y - cfc (fun (z : ℝ) => z * Real.log z) (conditionalAliceAverage G H y)).PosSemidef

noncomputable def QuantumParallelRepetition.fullCoordinateAliceEntropyIncrement {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullCoordinateAliceEntropyIncrement_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : ∑ x : X, G.marginalX x * ((bornTracePairing S.state.matrix) (cfc (fun (z : ℝ) => z * Real.log z) (fullCoordinateAliceQuestionFilter G n S D L i r α x))) (fullCoordinateBobMeanFilter G n S D L i r β x) - ∑ y : Y, G.marginalY y * ((bornTracePairing S.state.matrix) (cfc (fun (z : ℝ) => z * Real.log z) (fullCoordinateAliceMeanFilter G n S D L i r α y))) (fullCoordinateBobQuestionFilter G n S D L i r β y) = fullCoordinateAliceEntropyIncrement G n S D L i r α β

theorem QuantumParallelRepetition.fullCoordinateAliceEntropyIncrement_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : 0 ≤ fullCoordinateAliceEntropyIncrement G n S D L i r α β

def QuantumParallelRepetition.fullCoordinateBaseWinIndicator {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : ℝ

Equations

• QuantumParallelRepetition.fullCoordinateBaseWinIndicator G D L i r α β = if ∀ (j : ↥D), G.predicate (r.aliceConditioned j) (r.bobConditioned j) (α j) (β j) = true then 1 else 0

theorem QuantumParallelRepetition.fullCoordinateBaseWinIndicator_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (β : ↥D → B) : 0 ≤ fullCoordinateBaseWinIndicator G D L i r α β

theorem QuantumParallelRepetition.fullCoordinateOldHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (y : Y) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G (fullCoordinateOldHistory D L i r y) α β = fullCoordinateBaseWinIndicator G D L i r α β

theorem QuantumParallelRepetition.fullCoordinateNewHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (α : ↥D → A) (β : ↥D → B) : fullHistoryWinIndicator G (fullCoordinateNewHistory D L i r x) α β = fullCoordinateBaseWinIndicator G D L i r α β

theorem QuantumParallelRepetition.fullCoordinate_three_sum_rotate {I : Type u_5} {J : Type u_6} {K : Type u_7} {T : Type u_8} [Fintype I] [Fintype J] [Fintype K] [AddCommMonoid T] (f : I → J → K → T) : ∑ i : I, ∑ j : J, ∑ k : K, f i j k = ∑ j : J, ∑ k : K, ∑ i : I, f i j k

theorem QuantumParallelRepetition.fullCoordinateOldHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (f : FullSubsetHistory X Y n D L → T) : ∑ h : FullSubsetHistory X Y n D L, f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ y : Y, f (fullCoordinateOldHistory D L i r y)

theorem QuantumParallelRepetition.fullCoordinateNewHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (f : FullSubsetHistory X Y n D (insert i L) → T) : ∑ h : FullSubsetHistory X Y n D (insert i L), f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ x : X, f (fullCoordinateNewHistory D L i r x)

theorem QuantumParallelRepetition.fullCoordinateWeightedOldSum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (value : FullSubsetHistory X Y n D L → (↥D → A) → (↥D → B) → ℝ) : ∑ h : FullSubsetHistory X Y n D L, ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ y : Y, G.marginalY y * value (fullCoordinateOldHistory D L i r y) α β

theorem QuantumParallelRepetition.fullCoordinateWeightedNewSum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiL : i ∉ L) (value : FullSubsetHistory X Y n D (insert i L) → (↥D → A) → (↥D → B) → ℝ) : ∑ h : FullSubsetHistory X Y n D (insert i L), ∑ α : ↥D → A, ∑ β : ↥D → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ x : X, G.marginalX x * value (fullCoordinateNewHistory D L i r x) α β

noncomputable def QuantumParallelRepetition.fullCoordinateAliceTotalEntropyIncrement {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullHistoryAliceEntropyPotential_increment {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : fullHistoryAliceEntropyPotential G n S D (insert i L) - fullHistoryAliceEntropyPotential G n S D L = fullCoordinateAliceTotalEntropyIncrement G n S D L i

theorem QuantumParallelRepetition.fullCoordinateAliceTotalEntropyIncrement_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) : 0 ≤ fullCoordinateAliceTotalEntropyIncrement G n S D L i

@[reducible, inline]

abbrev QuantumParallelRepetition.SourceRemainingCoordinate {n : ℕ} (D : Finset (Fin n)) : Type

Equations

• QuantumParallelRepetition.SourceRemainingCoordinate D = ↥(Finset.univ \ D)

@[reducible, inline]

abbrev QuantumParallelRepetition.SourceRemainingPermutation {n : ℕ} (D : Finset (Fin n)) : Type

Equations

• QuantumParallelRepetition.SourceRemainingPermutation D = Equiv.Perm (QuantumParallelRepetition.SourceRemainingCoordinate D)

noncomputable def QuantumParallelRepetition.sourceRemainingPermutationRank {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) : SourceRemainingCoordinate D ≃ Fin (Finset.univ \ D).card

Equations

• QuantumParallelRepetition.sourceRemainingPermutationRank D π = (Equiv.symm π).trans (Finset.univ \ D).equivFin

noncomputable def QuantumParallelRepetition.sourceRemainingPermutationCoordinateSubtype {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : SourceRemainingCoordinate D

Equations

• QuantumParallelRepetition.sourceRemainingPermutationCoordinateSubtype D π k = (QuantumParallelRepetition.sourceRemainingPermutationRank D π).symm k

noncomputable def QuantumParallelRepetition.sourceRemainingPermutationCoordinate {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : Fin n

Equations

• QuantumParallelRepetition.sourceRemainingPermutationCoordinate D π k = ↑(QuantumParallelRepetition.sourceRemainingPermutationCoordinateSubtype D π k)

@[simp]

theorem QuantumParallelRepetition.sourceRemainingPermutationRank_coordinate {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : (sourceRemainingPermutationRank D π) (sourceRemainingPermutationCoordinateSubtype D π k) = k

theorem QuantumParallelRepetition.sourceRemainingPermutationCoordinate_not_mem {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : sourceRemainingPermutationCoordinate D π k ∉ D

noncomputable def QuantumParallelRepetition.sourceRemainingPermutationPrefixSubtype {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin ((Finset.univ \ D).card + 1)) : Finset (SourceRemainingCoordinate D)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.sourceRemainingPermutationPrefix {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin ((Finset.univ \ D).card + 1)) : Finset (Fin n)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.sourceRemainingPermutationPrefix_subset {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin ((Finset.univ \ D).card + 1)) : sourceRemainingPermutationPrefix D π k ⊆ Finset.univ \ D

theorem QuantumParallelRepetition.sourceRemainingPermutationCoordinate_not_mem_prefix {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : sourceRemainingPermutationCoordinate D π k ∉ sourceRemainingPermutationPrefix D π k.castSucc

theorem QuantumParallelRepetition.sourceRemainingPermutationPrefixSubtype_succ {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : sourceRemainingPermutationPrefixSubtype D π k.succ = insert (sourceRemainingPermutationCoordinateSubtype D π k) (sourceRemainingPermutationPrefixSubtype D π k.castSucc)

theorem QuantumParallelRepetition.sourceRemainingPermutationPrefix_succ {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : sourceRemainingPermutationPrefix D π k.succ = insert (sourceRemainingPermutationCoordinate D π k) (sourceRemainingPermutationPrefix D π k.castSucc)

@[simp]

theorem QuantumParallelRepetition.sourceRemainingPermutationPrefix_zero {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) : sourceRemainingPermutationPrefix D π 0 = ∅

@[simp]

theorem QuantumParallelRepetition.sourceRemainingPermutationPrefix_last {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) : sourceRemainingPermutationPrefix D π (Fin.last (Finset.univ \ D).card) = Finset.univ \ D

theorem QuantumParallelRepetition.sourceRemainingPermutationCoordinate_sum {T : Type u_1} [AddCommMonoid T] {n : ℕ} (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (f : Fin n → T) : ∑ k : Fin (Finset.univ \ D).card, f (sourceRemainingPermutationCoordinate D π k) = ∑ i : SourceRemainingCoordinate D, f ↑i

theorem QuantumParallelRepetition.fin_sum_successive_sub {m : ℕ} (f : Fin (m + 1) → ℝ) : ∑ k : Fin m, (f k.succ - f k.castSucc) = f (Fin.last m) - f 0

noncomputable def QuantumParallelRepetition.sourcePermutationAliceEntropyIncrement {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.sourcePermutationAliceEntropyIncrement_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : 0 ≤ sourcePermutationAliceEntropyIncrement G n S D π k

theorem QuantumParallelRepetition.sourcePermutationAliceEntropyPotential_step {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) : fullHistoryAliceEntropyPotential G n S D (sourceRemainingPermutationPrefix D π k.succ) - fullHistoryAliceEntropyPotential G n S D (sourceRemainingPermutationPrefix D π k.castSucc) = sourcePermutationAliceEntropyIncrement G n S D π k

theorem QuantumParallelRepetition.sourcePermutationAliceEntropyIncrement_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (π : SourceRemainingPermutation D) : ∑ k : Fin (Finset.univ \ D).card, sourcePermutationAliceEntropyIncrement G n S D π k = fullHistoryAliceEntropyPotential G n S D (Finset.univ \ D) - fullHistoryAliceEntropyPotential G n S D ∅

theorem QuantumParallelRepetition.sourcePermutationAliceEntropyIncrement_sum_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) (π : SourceRemainingPermutation D) : ∑ k : Fin (Finset.univ \ D).card, sourcePermutationAliceEntropyIncrement G n S D π k ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))

noncomputable def QuantumParallelRepetition.sourceUniformPermutationAverage {n : ℕ} (D : Finset (Fin n)) (f : SourceRemainingPermutation D → Fin (Finset.univ \ D).card → ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.sourceRemainingPermutation_card_pos {n : ℕ} (D : Finset (Fin n)) : 0 < ↑(Fintype.card (SourceRemainingPermutation D))

theorem QuantumParallelRepetition.sourceUniformPermutationAverage_le {n : ℕ} (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) (f : SourceRemainingPermutation D → Fin (Finset.univ \ D).card → ℝ) {C : ℝ} (hC : ∀ (π : SourceRemainingPermutation D), ∑ k : Fin (Finset.univ \ D).card, f π k ≤ C) : sourceUniformPermutationAverage D f ≤ C / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.sourceUniformPermutationAverage_nonneg {n : ℕ} (D : Finset (Fin n)) (f : SourceRemainingPermutation D → Fin (Finset.univ \ D).card → ℝ) (hf : ∀ (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card), 0 ≤ f π k) : 0 ≤ sourceUniformPermutationAverage D f

theorem QuantumParallelRepetition.sourceUniformPermutationAliceEntropyBudget {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) (hp : 0 < (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) : sourceUniformPermutationAverage D (sourcePermutationAliceEntropyIncrement G n S D) ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) * Real.log (fullHistoryAnswerCount D / (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D)) / ↑(Finset.univ \ D).card

def QuantumParallelRepetition.exactLeft {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : Finset M

Equations

• QuantumParallelRepetition.exactLeft coordinate partition = {j : M | j ≠ coordinate ∧ partition j = false}

def QuantumParallelRepetition.exactRight {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : Finset M

Equations

• QuantumParallelRepetition.exactRight coordinate partition = {j : M | j ≠ coordinate ∧ partition j = true}

theorem QuantumParallelRepetition.exactLeft_coordinate_not_mem {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : coordinate ∉ exactLeft coordinate partition

theorem QuantumParallelRepetition.exactRight_coordinate_not_mem {M : Type u_1} [Fintype M] [DecidableEq M] (coordinate : M) (partition : M → Bool) : coordinate ∉ exactRight coordinate partition

structure QuantumParallelRepetition.ExactForwardSeed (M : Type u_1) [Fintype M] [DecidableEq M] : Type u_1

• coordinate : M
• partition : M → Bool
• leftOrder : Equiv.Perm ↥(exactLeft self.coordinate self.partition)
• rightOrder : Equiv.Perm ↥(exactRight self.coordinate self.partition)
• leftCut : Fin ((exactLeft self.coordinate self.partition).card + 1)
• rightCut : Fin ((exactRight self.coordinate self.partition).card + 1)

@[instance_reducible]

instance QuantumParallelRepetition.instFintypeExactForwardSeed {M✝ : Type u_1} {inst✝ : Fintype M✝} {inst✝¹ : DecidableEq M✝} [Fintype M✝] : Fintype (ExactForwardSeed M✝)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactRemainingSeed {n : ℕ} (D : Finset (Fin n)) : Type

Equations

• QuantumParallelRepetition.ExactRemainingSeed D = QuantumParallelRepetition.ExactForwardSeed (QuantumParallelRepetition.SourceRemainingCoordinate D)

noncomputable def QuantumParallelRepetition.exactLeftRank {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↥(exactLeft seed.coordinate seed.partition) ≃ Fin (exactLeft seed.coordinate seed.partition).card

Equations

• QuantumParallelRepetition.exactLeftRank seed = (Equiv.symm seed.leftOrder).trans (QuantumParallelRepetition.exactLeft seed.coordinate seed.partition).equivFin

noncomputable def QuantumParallelRepetition.exactRightRank {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ↥(exactRight seed.coordinate seed.partition) ≃ Fin (exactRight seed.coordinate seed.partition).card

Equations

• QuantumParallelRepetition.exactRightRank seed = (Equiv.symm seed.rightOrder).trans (QuantumParallelRepetition.exactRight seed.coordinate seed.partition).equivFin

noncomputable def QuantumParallelRepetition.exactLeftPrefix {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : Finset M

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactRightPrefix {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : Finset M

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactLeftPrefix_subset {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactLeftPrefix seed ⊆ exactLeft seed.coordinate seed.partition

theorem QuantumParallelRepetition.exactRightPrefix_subset {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : exactRightPrefix seed ⊆ exactRight seed.coordinate seed.partition

noncomputable def QuantumParallelRepetition.exactSeedWeight {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactSeedWeight_nonneg {M : Type u_1} [Fintype M] [DecidableEq M] (seed : ExactForwardSeed M) : 0 ≤ exactSeedWeight seed

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactSeedTuple (M : Type u_1) [Fintype M] [DecidableEq M] : Type u_1

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.exactSeedEquiv (M : Type u_1) [Fintype M] [DecidableEq M] : ExactForwardSeed M ≃ ExactSeedTuple M

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumParallelRepetition.exactSeedEquiv_symm_apply {M : Type u_1} [Fintype M] [DecidableEq M] (t : ExactSeedTuple M) : (exactSeedEquiv M).symm t = { coordinate := t.fst, partition := t.snd.fst, leftOrder := t.snd.snd.1, rightOrder := t.snd.snd.2.1, leftCut := t.snd.snd.2.2.1, rightCut := t.snd.snd.2.2.2 }

theorem QuantumParallelRepetition.exactForwardSeed_sum {M : Type u_1} [Fintype M] [DecidableEq M] (f : ExactForwardSeed M → ℝ) : ∑ seed : ExactForwardSeed M, f seed = ∑ i : M, ∑ partition : M → Bool, ∑ leftOrder : Equiv.Perm ↥(exactLeft i partition), ∑ rightOrder : Equiv.Perm ↥(exactRight i partition), ∑ leftCut : Fin ((exactLeft i partition).card + 1), ∑ rightCut : Fin ((exactRight i partition).card + 1), f { coordinate := i, partition := partition, leftOrder := leftOrder, rightOrder := rightOrder, leftCut := leftCut, rightCut := rightCut }

theorem QuantumParallelRepetition.exactUniform_sum {T : Type u_1} [Fintype T] (positive : 0 < Fintype.card T) : ∑ _t : T, 1 / ↑(Fintype.card T) = 1

theorem QuantumParallelRepetition.exactUniform_sum_mul {T : Type u_1} [Fintype T] (positive : 0 < Fintype.card T) (value : ℝ) : ∑ _t : T, value * (1 / ↑(Fintype.card T)) = value

theorem QuantumParallelRepetition.exactPrefixUniform_sum_mul (m : ℕ) (value : ℝ) : ∑ _k : Fin (m + 1), value * (1 / (↑m + 1)) = value

theorem QuantumParallelRepetition.exactPermutationUniform_sum_mul {T : Type u_1} [Fintype T] (value : ℝ) : ∑ _π : Equiv.Perm T, value * (1 / ↑(Fintype.card (Equiv.Perm T))) = value

theorem QuantumParallelRepetition.common_finite_purification_pair_jensen {ι : Type u_1} {κ : Type u_2} {d : Type u_3} [Fintype ι] [Fintype κ] [Fintype d] [DecidableEq d] (weight : ι → ℝ) (F : κ → Matrix d d ℂ) (anchor : Matrix d d ℂ) (positive : ∀ (k : κ), (F k).PosSemidef) (hanchor : anchor.PosSemidef) (choose : ι → κ) (meanIndex : κ) (nonnegative : ∀ (a : ι), 0 ≤ weight a) (normalized : ∑ a : ι, weight a = 1) (mean : ∑ a : ι, weight a • F (choose a) = F meanIndex) : (∑ a : ι, weight a • cfc (fun (z : ℝ) => z * Real.log z) (F (choose a)) - cfc (fun (z : ℝ) => z * Real.log z) (F meanIndex) - ∑ a : ι, weight a • ((finitePurificationMatrix F anchor positive hanchor (choose a) - finitePurificationMatrix F anchor positive hanchor meanIndex).conjTranspose * (finitePurificationMatrix F anchor positive hanchor (choose a) - finitePurificationMatrix F anchor positive hanchor meanIndex))).PosSemidef

theorem QuantumParallelRepetition.commonFinitePurification_weighted_left_variation_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {ι : Type u_5} {κ : Type u_6} {eB : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype ι] [Fintype κ] [Fintype eB] {G : Game X Y A B} (S : Strategy G) (weight : ι → ℝ) (F : κ → Matrix S.Alice S.Alice ℂ) (anchor : Matrix S.Alice S.Alice ℂ) (positive : ∀ (k : κ), (F k).PosSemidef) (hanchor : anchor.PosSemidef) (choose : ι → κ) (meanIndex : κ) (nonnegative : ∀ (a : ι), 0 ≤ weight a) (normalized : ∑ a : ι, weight a = 1) (mean : ∑ a : ι, weight a • F (choose a) = F meanIndex) (KB : Matrix eB S.Bob ℂ) : ∑ a : ι, weight a * ‖finiteLocalPurificationVector S (finitePurificationMatrix F anchor positive hanchor (choose a)) KB - finiteLocalPurificationVector S (finitePurificationMatrix F anchor positive hanchor meanIndex) KB‖ ^ 2 ≤ ((bornTracePairing S.state.matrix) (∑ a : ι, weight a • cfc (fun (z : ℝ) => z * Real.log z) (F (choose a)) - cfc (fun (z : ℝ) => z * Real.log z) (F meanIndex))) (KB.conjTranspose * KB)

theorem QuantumParallelRepetition.commonFinitePurification_weighted_right_variation_le {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {ι : Type u_5} {κ : Type u_6} {eA : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype ι] [Fintype κ] [Fintype eA] {G : Game X Y A B} (S : Strategy G) (weight : ι → ℝ) (F : κ → Matrix S.Bob S.Bob ℂ) (anchor : Matrix S.Bob S.Bob ℂ) (positive : ∀ (k : κ), (F k).PosSemidef) (hanchor : anchor.PosSemidef) (choose : ι → κ) (meanIndex : κ) (nonnegative : ∀ (b : ι), 0 ≤ weight b) (normalized : ∑ b : ι, weight b = 1) (mean : ∑ b : ι, weight b • F (choose b) = F meanIndex) (KA : Matrix eA S.Alice ℂ) : ∑ b : ι, weight b * ‖finiteLocalPurificationVector S KA (finitePurificationMatrix F anchor positive hanchor (choose b)) - finiteLocalPurificationVector S KA (finitePurificationMatrix F anchor positive hanchor meanIndex)‖ ^ 2 ≤ ((bornTracePairing S.state.matrix) (KA.conjTranspose * KA)) (∑ b : ι, weight b • cfc (fun (z : ℝ) => z * Real.log z) (F (choose b)) - cfc (fun (z : ℝ) => z * Real.log z) (F meanIndex))

theorem QuantumParallelRepetition.rectangular_matrix_quadratic_compression {d : Type u_1} {e : Type u_2} [Fintype d] [Fintype e] [DecidableEq d] [DecidableEq e] (K : Matrix e d ℂ) (E : Matrix e e ℂ) (z : EuclideanSpace ℂ d) : quadraticExpectation (Matrix.toEuclideanCLM E) (WithLp.toLp 2 (K.mulVec z.ofLp)) = quadraticExpectation (Matrix.toEuclideanCLM (K.conjTranspose * E * K)) z

theorem QuantumParallelRepetition.finiteLocalPurificationJointMatrix_compression {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] [DecidableEq eA] [DecidableEq eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) (EA : Matrix eA eA ℂ) (EB : Matrix eB eB ℂ) : (finiteLocalPurificationJointMatrix S KA KB).conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA 1) EB * finiteLocalPurificationJointMatrix S KA KB = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (KA.conjTranspose * EA * KA) 1) (KB.conjTranspose * EB * KB)

theorem QuantumParallelRepetition.finiteLocalPurificationVector_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} {eA : Type u_5} {eB : Type u_6} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype eA] [Fintype eB] [DecidableEq eA] [DecidableEq eB] {G : Game X Y A B} (S : Strategy G) (KA : Matrix eA S.Alice ℂ) (KB : Matrix eB S.Bob ℂ) (EA : Matrix eA eA ℂ) (EB : Matrix eB eB ℂ) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA 1) EB)) (finiteLocalPurificationVector S KA KB) = ((bornTracePairing S.state.matrix) (KA.conjTranspose * EA * KA)) (KB.conjTranspose * EB * KB)

noncomputable def QuantumParallelRepetition.conditionedAliceCoordinateEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (xs : Fin n → X) (i : Fin n) (a : A) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.conditionedBobCoordinateEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (β : ↥D → B) (ys : Fin n → Y) (i : Fin n) (b : B) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.conditionedAliceCoordinateEffect_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (xs : Fin n → X) (i : Fin n) (a : A) : (conditionedAliceCoordinateEffect G n S D α xs i a).PosSemidef

theorem QuantumParallelRepetition.conditionedBobCoordinateEffect_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (β : ↥D → B) (ys : Fin n → Y) (i : Fin n) (b : B) : (conditionedBobCoordinateEffect G n S D β ys i b).PosSemidef

theorem QuantumParallelRepetition.conditionedAliceCoordinateEffect_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (xs : Fin n → X) (i : Fin n) : ∑ a : A, conditionedAliceCoordinateEffect G n S D α xs i a = conditionedAliceEffect G n S D α xs

theorem QuantumParallelRepetition.conditionedBobCoordinateEffect_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (β : ↥D → B) (ys : Fin n → Y) (i : Fin n) : ∑ b : B, conditionedBobCoordinateEffect G n S D β ys i b = conditionedBobEffect G n S D β ys

noncomputable def QuantumParallelRepetition.fullHistoryAliceCoordinateEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (α : ↥D → A) (i : Fin n) (a : A) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.fullHistoryBobCoordinateEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (h : FullSubsetHistory X Y n D L) (β : ↥D → B) (i : Fin n) (b : B) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.fullCoordinateAliceRefinementEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (α : ↥D → A) (x : X) (a : A) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.fullCoordinateBobRefinementEffect {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (β : ↥D → B) (y : Y) (b : B) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

structure QuantumParallelRepetition.ExactRevealHistory (X : Type u_5) (Y : Type u_6) [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : Type (max u_5 u_6)

• aliceConditioned : ↥D → X
• bobConditioned : ↥D → Y
• aliceLeft : ↥(exactLeft seed.coordinate seed.partition) → X
• bobRight : ↥(exactRight seed.coordinate seed.partition) → Y
• bobLeftPrefix : ↥(exactLeftPrefix seed) → Y
• aliceRightPrefix : ↥(exactRightPrefix seed) → X

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactRevealHistoryTuple (X : Type u_5) (Y : Type u_6) [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : Type (max u_5 u_5 u_6)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.exactRevealHistoryEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : ExactRevealHistory X Y D seed ≃ ExactRevealHistoryTuple X Y D seed

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance QuantumParallelRepetition.exactRevealHistoryFintype {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : Fintype (ExactRevealHistory X Y D seed)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactFullQuestion (X : Type u_5) (Y : Type u_6) (n : ℕ) : Type (max u_5 u_6)

Equations

• QuantumParallelRepetition.ExactFullQuestion X Y n = ((Fin n → X) × (Fin n → Y))

def QuantumParallelRepetition.exactRevealCode {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (q : ExactFullQuestion X Y n) : ExactRevealHistory X Y D seed

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.exactPriorQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (q : ExactFullQuestion X Y n) : ℝ

Equations

• QuantumParallelRepetition.exactPriorQuestionWeight G n q = (G.repeat n).questionWeight q.1 q.2

theorem QuantumParallelRepetition.exactPriorQuestionWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (q : ExactFullQuestion X Y n) : 0 ≤ exactPriorQuestionWeight G n q

theorem QuantumParallelRepetition.exactPriorQuestionWeight_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) : ∑ q : ExactFullQuestion X Y n, exactPriorQuestionWeight G n q = 1

noncomputable def QuantumParallelRepetition.exactRevealMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactRevealMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) : 0 ≤ exactRevealMass G n D seed history

theorem QuantumParallelRepetition.exactRevealMass_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) : ∑ history : ExactRevealHistory X Y D seed, exactRevealMass G n D seed history = 1

noncomputable def QuantumParallelRepetition.exactAliceQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactBobQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactJointQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactAliceQuestionMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) : 0 ≤ exactAliceQuestionMass G n D seed history x

theorem QuantumParallelRepetition.exactBobQuestionMass_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) : 0 ≤ exactBobQuestionMass G n D seed history y

noncomputable def QuantumParallelRepetition.exactAliceQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactBobQuestionFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactAliceQuestionFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) : (exactAliceQuestionFilter G n S D seed history answer x).PosSemidef

theorem QuantumParallelRepetition.exactBobQuestionFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) : (exactBobQuestionFilter G n S D seed history answer y).PosSemidef

noncomputable def QuantumParallelRepetition.exactAliceMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (y : Y) : Matrix S.Alice S.Alice ℂ

Equations

• QuantumParallelRepetition.exactAliceMeanFilter G n S D seed history answer y = ∑ x : X, G.conditionalXGivenY y x • QuantumParallelRepetition.exactAliceQuestionFilter G n S D seed history answer x

noncomputable def QuantumParallelRepetition.exactBobMeanFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (x : X) : Matrix S.Bob S.Bob ℂ

Equations

• QuantumParallelRepetition.exactBobMeanFilter G n S D seed history answer x = ∑ y : Y, G.conditionalYGivenX x y • QuantumParallelRepetition.exactBobQuestionFilter G n S D seed history answer y

theorem QuantumParallelRepetition.exactAliceMeanFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (y : Y) : (exactAliceMeanFilter G n S D seed history answer y).PosSemidef

theorem QuantumParallelRepetition.exactBobMeanFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (x : X) : (exactBobMeanFilter G n S D seed history answer x).PosSemidef

noncomputable def QuantumParallelRepetition.exactAliceCoordinateFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) (a : A) : Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactBobCoordinateFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) (b : B) : Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactAliceCoordinateFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) (a : A) : (exactAliceCoordinateFilter G n S D seed history answer x a).PosSemidef

theorem QuantumParallelRepetition.exactBobCoordinateFilter_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) (b : B) : (exactBobCoordinateFilter G n S D seed history answer y b).PosSemidef

theorem QuantumParallelRepetition.exactAliceCoordinateFilter_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (x : X) : ∑ a : A, exactAliceCoordinateFilter G n S D seed history answer x a = exactAliceQuestionFilter G n S D seed history answer x

theorem QuantumParallelRepetition.exactBobCoordinateFilter_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (y : Y) : ∑ b : B, exactBobCoordinateFilter G n S D seed history answer y b = exactBobQuestionFilter G n S D seed history answer y

noncomputable def QuantumParallelRepetition.exactAlicePurificationFamily {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) : X ⊕ Y → Matrix S.Alice S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactBobPurificationFamily {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) : Y ⊕ X → Matrix S.Bob S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactAlicePurificationFamily_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (q : X ⊕ Y) : (exactAlicePurificationFamily G n S D seed history answer q).PosSemidef

theorem QuantumParallelRepetition.exactBobPurificationFamily_posSemidef {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (q : Y ⊕ X) : (exactBobPurificationFamily G n S D seed history answer q).PosSemidef

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactAliceLiftIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) : Type

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactBobLiftIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) : Type

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactAlicePurificationMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (q : X ⊕ Y) : Matrix (ExactAliceLiftIndex G n S D seed history answer) S.Alice ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactBobPurificationMatrix {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (q : Y ⊕ X) : Matrix (ExactBobLiftIndex G n S D seed history answer) S.Bob ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactAlicePurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → A) (q : X ⊕ Y) : (exactAlicePurificationMatrix G n S D seed history answer q).conjTranspose * exactAlicePurificationMatrix G n S D seed history answer q = exactAlicePurificationFamily G n S D seed history answer q

theorem QuantumParallelRepetition.exactBobPurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (answer : ↥D → B) (q : Y ⊕ X) : (exactBobPurificationMatrix G n S D seed history answer q).conjTranspose * exactBobPurificationMatrix G n S D seed history answer q = exactBobPurificationFamily G n S D seed history answer q

structure QuantumParallelRepetition.ExactHistoryFlag (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max (max (max u_5 u_6) u_7) u_8)

• seed : ExactRemainingSeed D
• history : ExactRevealHistory X Y D self.seed
• aliceAnswer : ↥D → A
• bobAnswer : ↥D → B

theorem QuantumParallelRepetition.ExactHistoryFlag.ext {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} {inst✝ : Fintype X} {inst✝¹ : Fintype Y} {inst✝² : Fintype A} {inst✝³ : Fintype B} {n : ℕ} {D : Finset (Fin n)} {x y : ExactHistoryFlag X Y A B D} (seed : x.seed = y.seed) (history : x.history ≍ y.history) (aliceAnswer : x.aliceAnswer = y.aliceAnswer) (bobAnswer : x.bobAnswer = y.bobAnswer) : x = y

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactHistoryFlagTuple (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max (max u_8 u_7) u_6 u_5)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.exactHistoryFlagEquiv {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ExactHistoryFlag X Y A B D ≃ ExactHistoryFlagTuple X Y A B D

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance QuantumParallelRepetition.exactHistoryFlagFintype {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Fintype (ExactHistoryFlag X Y A B D)

Equations

• QuantumParallelRepetition.exactHistoryFlagFintype D = Fintype.ofEquiv (QuantumParallelRepetition.ExactHistoryFlagTuple X Y A B D) (QuantumParallelRepetition.exactHistoryFlagEquiv D).symm

theorem QuantumParallelRepetition.exactHistoryFlag_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (f : ExactHistoryFlag X Y A B D → ℝ) : ∑ r : ExactHistoryFlag X Y A B D, f r = ∑ seed : ExactRemainingSeed D, ∑ history : ExactRevealHistory X Y D seed, ∑ aliceAnswer : ↥D → A, ∑ bobAnswer : ↥D → B, f { seed := seed, history := history, aliceAnswer := aliceAnswer, bobAnswer := bobAnswer }

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactAliceLocalIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Type

Equations

• QuantumParallelRepetition.ExactAliceLocalIndex G n S D r = (QuantumParallelRepetition.ExactAliceLiftIndex G n S D r.seed r.history r.aliceAnswer × S.Alice × S.Bob)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactBobLocalIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Type

Equations

• QuantumParallelRepetition.ExactBobLocalIndex G n S D r = QuantumParallelRepetition.ExactBobLiftIndex G n S D r.seed r.history r.bobAnswer

noncomputable def QuantumParallelRepetition.exactUnnormalizedPsi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactUnnormalizedPhi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (y : Y) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactUnnormalizedGamma {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactUnnormalizedPsi_norm_sq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : ‖exactUnnormalizedPsi G n S D r x y‖ ^ 2 = ((bornTracePairing S.state.matrix) (exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x)) (exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y)

theorem QuantumParallelRepetition.exactAliceQuestionPurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) : (exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x)).conjTranspose * exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x) = exactAliceQuestionFilter G n S D r.seed r.history r.aliceAnswer x

theorem QuantumParallelRepetition.exactBobQuestionPurificationMatrix_gram {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (y : Y) : (exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y)).conjTranspose * exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y) = exactBobQuestionFilter G n S D r.seed r.history r.bobAnswer y

noncomputable def QuantumParallelRepetition.exactAliceRefinedPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (x : X) : POVM A (ExactAliceLiftIndex G n S D r.seed r.history r.aliceAnswer)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactBobRefinedPOVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (b₀ : B) (y : Y) : POVM B (ExactBobLiftIndex G n S D r.seed r.history r.bobAnswer)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactAliceRefinedPOVM_compression {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (x : X) (a : A) : (exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x)).conjTranspose * (exactAliceRefinedPOVM G n S D r a₀ x).effect a * exactAlicePurificationMatrix G n S D r.seed r.history r.aliceAnswer (Sum.inl x) = exactAliceCoordinateFilter G n S D r.seed r.history r.aliceAnswer x a

theorem QuantumParallelRepetition.exactBobRefinedPOVM_compression {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (b₀ : B) (y : Y) (b : B) : (exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y)).conjTranspose * (exactBobRefinedPOVM G n S D r b₀ y).effect b * exactBobPurificationMatrix G n S D r.seed r.history r.bobAnswer (Sum.inl y) = exactBobCoordinateFilter G n S D r.seed r.history r.bobAnswer y b

theorem QuantumParallelRepetition.exactRefinedPOVM_quadratic {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (a₀ : A) (b₀ : B) (x : X) (y : Y) (a : A) (b : B) : quadraticExpectation (Matrix.toEuclideanCLM (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((exactAliceRefinedPOVM G n S D r a₀ x).effect a) 1) ((exactBobRefinedPOVM G n S D r b₀ y).effect b))) (exactUnnormalizedPsi G n S D r x y) = ((bornTracePairing S.state.matrix) (exactAliceCoordinateFilter G n S D r.seed r.history r.aliceAnswer x a)) (exactBobCoordinateFilter G n S D r.seed r.history r.bobAnswer y b)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactPaddedLocalIndex {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : Type

Equations

• QuantumParallelRepetition.ExactPaddedLocalIndex G n S D r = (PUnit.{1} ⊕ QuantumParallelRepetition.ExactAliceLocalIndex G n S D r ⊕ QuantumParallelRepetition.ExactBobLocalIndex G n S D r)

def QuantumParallelRepetition.exactPaddedVector {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactPaddedVector_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (z : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : ‖exactPaddedVector G n S D r z‖ = ‖z‖

theorem QuantumParallelRepetition.exactPaddedVector_sub {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (u v : EuclideanSpace ℂ (ExactAliceLocalIndex G n S D r × ExactBobLocalIndex G n S D r)) : exactPaddedVector G n S D r (u - v) = exactPaddedVector G n S D r u - exactPaddedVector G n S D r v

noncomputable def QuantumParallelRepetition.exactPaddedDefault {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

Equations

• QuantumParallelRepetition.exactPaddedDefault G n S D r = PiLp.single 2 (Sum.inl PUnit.unit, Sum.inl PUnit.unit) 1

theorem QuantumParallelRepetition.exactPaddedDefault_norm {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) : ‖exactPaddedDefault G n S D r‖ = 1

noncomputable def QuantumParallelRepetition.exactPsi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) (y : Y) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactPhi {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (y : Y) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.exactGamma {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : ExactHistoryFlag X Y A B D) (x : X) : EuclideanSpace ℂ (ExactPaddedLocalIndex G n S D r × ExactPaddedLocalIndex G n S D r)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.exactAliceQuestionCompatible {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (xs : Fin n → X) : Prop

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.exactBobQuestionCompatible {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (y : Y) (ys : Fin n → Y) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactRevealCode_compatible_iff {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : exactRevealCode D seed (xs, ys) = history ∧ xs ↑seed.coordinate = x ∧ ys ↑seed.coordinate = y ↔ exactAliceQuestionCompatible D seed history x xs ∧ exactBobQuestionCompatible D seed history y ys

theorem QuantumParallelRepetition.exactCompatible_coordinate_eq_or {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y ys') (j : Fin n) : xs j = xs' j ∨ ys j = ys' j

theorem QuantumParallelRepetition.exactQuestionWeight_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) (ha : exactAliceQuestionCompatible D seed history x xs) (ha' : exactAliceQuestionCompatible D seed history x xs') (hb : exactBobQuestionCompatible D seed history y ys) (hb' : exactBobQuestionCompatible D seed history y ys') : (G.repeat n).questionWeight xs ys * (G.repeat n).questionWeight xs' ys' = (G.repeat n).questionWeight xs ys' * (G.repeat n).questionWeight xs' ys

noncomputable def QuantumParallelRepetition.exactFiberQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactFiberQuestionWeight_rectangle {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs xs' : Fin n → X) (ys ys' : Fin n → Y) : exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionWeight G n D seed history x y xs' ys' = exactFiberQuestionWeight G n D seed history x y xs ys' * exactFiberQuestionWeight G n D seed history x y xs' ys

noncomputable def QuantumParallelRepetition.exactFiberAliceMarginal {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) : ℝ

Equations

• QuantumParallelRepetition.exactFiberAliceMarginal G n D seed history x y xs = ∑ ys : Fin n → Y, QuantumParallelRepetition.exactFiberQuestionWeight G n D seed history x y xs ys

noncomputable def QuantumParallelRepetition.exactFiberBobMarginal {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (ys : Fin n → Y) : ℝ

Equations

• QuantumParallelRepetition.exactFiberBobMarginal G n D seed history x y ys = ∑ xs : Fin n → X, QuantumParallelRepetition.exactFiberQuestionWeight G n D seed history x y xs ys

noncomputable def QuantumParallelRepetition.exactFiberQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) : ℝ

Equations

• QuantumParallelRepetition.exactFiberQuestionMass G n D seed history x y = ∑ xs : Fin n → X, ∑ ys : Fin n → Y, QuantumParallelRepetition.exactFiberQuestionWeight G n D seed history x y xs ys

theorem QuantumParallelRepetition.exactFiberQuestionWeight_mul_mass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (seed : ExactRemainingSeed D) (history : ExactRevealHistory X Y D seed) (x : X) (y : Y) (xs : Fin n → X) (ys : Fin n → Y) : exactFiberQuestionWeight G n D seed history x y xs ys * exactFiberQuestionMass G n D seed history x y = exactFiberAliceMarginal G n D seed history x y xs * exactFiberBobMarginal G n D seed history x y ys

theorem QuantumParallelRepetition.exactFintypeCard_eq {T : Type u_1} (first second : Fintype T) : Fintype.card T = Fintype.card T

theorem QuantumParallelRepetition.exactSeedWeight_sum {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) : ∑ seed : ExactForwardSeed M, exactSeedWeight seed = 1

def QuantumParallelRepetition.HasExponentialBound (v : ℕ → ℝ) : Prop

Equations

• QuantumParallelRepetition.HasExponentialBound v = ∃ (c : ℝ), 0 < c ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), v n ≤ C * Real.exp (-c * ↑n)

def QuantumParallelRepetition.HasSubexponentialWitness (v : ℕ → ℝ) : Prop

Equations

• QuantumParallelRepetition.HasSubexponentialWitness v = ∀ (c : ℝ), 0 < c → ∀ (C : ℝ), 0 < C → ∃ (n : ℕ), C * Real.exp (-c * ↑n) < v n

theorem QuantumParallelRepetition.not_hasExponentialBound_iff (v : ℕ → ℝ) : ¬HasExponentialBound v ↔ HasSubexponentialWitness v

theorem QuantumParallelRepetition.arbitrarily_large_witness_of_not_hasExponentialBound {v : ℕ → ℝ} (hv : ∀ (n : ℕ), v n ≤ 1) (h_no_bound : ¬HasExponentialBound v) {c : ℝ} (hc : 0 < c) (N : ℕ) : ∃ (n : ℕ), N < n ∧ Real.exp (-c * ↑n) < v n

def QuantumParallelRepetition.StandardQuantumParallelRepetition {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.sum_positive_difference_eq_totalVariation {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) (hp : ∑ i : ι, p i = 1) (hq : ∑ i : ι, q i = 1) : ∑ i : ι, max (p i - q i) 0 = Pinsker.finiteTotalVariation p q

theorem QuantumParallelRepetition.finiteTotalVariation_comm {ι : Type u_1} [Fintype ι] (p q : ι → ℝ) : Pinsker.finiteTotalVariation p q = Pinsker.finiteTotalVariation q p

theorem QuantumParallelRepetition.expectation_le_add_totalVariation {ι : Type u_1} [Fintype ι] (p q f : ι → ℝ) (hp : ∑ i : ι, p i = 1) (hq : ∑ i : ι, q i = 1) (U : ℝ) (hfzero : ∀ (i : ι), 0 ≤ f i) (hfupper : ∀ (i : ι), f i ≤ U) : ∑ i : ι, p i * f i ≤ ∑ i : ι, q i * f i + U * Pinsker.finiteTotalVariation p q

theorem QuantumParallelRepetition.winning_expectation_transfer {ι : Type u_1} [Fintype ι] (p q win : ι → ℝ) (hp : ∑ i : ι, p i = 1) (hq : ∑ i : ι, q i = 1) (hzero : ∀ (i : ι), 0 ≤ win i) (hone : ∀ (i : ι), win i ≤ 1) : ∑ i : ι, q i * win i - Pinsker.finiteTotalVariation p q ≤ ∑ i : ι, p i * win i

def QuantumParallelRepetition.pureVerifierEffect {X Y A B dA dB : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (G : Game X Y A B) (z : EuclideanSpace ℂ (dA × dB)) (hz : ‖z‖ = 1) (PA : X → POVM A dA) (PB : Y → POVM B dB) (x : X) (y : Y) : Matrix (dA × dB) (dA × dB) ℂ

Equations

• QuantumParallelRepetition.pureVerifierEffect G z hz PA PB x y = (QuantumParallelRepetition.pureVectorStrategy G z hz PA PB).winningEffect x y

theorem QuantumParallelRepetition.pureVectorWinningProbability_eq {X Y A B dA dB : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (G : Game X Y A B) (z : EuclideanSpace ℂ (dA × dB)) (hz : ‖z‖ = 1) (PA : X → POVM A dA) (PB : Y → POVM B dB) : (pureVectorStrategy G z hz PA PB).winProbability = ∑ x : X, ∑ y : Y, G.questionWeight x y * quadraticExpectation (Matrix.toEuclideanCLM (pureVerifierEffect G z hz PA PB x y)) z

def QuantumParallelRepetition.flaggedQuestionWeight {X Y A B J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (flagWeight : J → ℝ) (ω : J × X × Y) : ℝ

Equations

• QuantumParallelRepetition.flaggedQuestionWeight G flagWeight ω = flagWeight ω.1 * G.questionWeight ω.2.1 ω.2.2

theorem QuantumParallelRepetition.flaggedQuestionWeight_nonneg {X Y A B J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (flagWeight : J → ℝ) (nonnegative : ∀ (j : J), 0 ≤ flagWeight j) (ω : J × X × Y) : 0 ≤ flaggedQuestionWeight G flagWeight ω

theorem QuantumParallelRepetition.flaggedQuestionWeight_sum {X Y A B J : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Fintype J] (G : Game X Y A B) (flagWeight : J → ℝ) (normalized : ∑ j : J, flagWeight j = 1) : ∑ ω : J × X × Y, flaggedQuestionWeight G flagWeight ω = 1

noncomputable def QuantumParallelRepetition.universalErrorCeiling (K₀ : ℝ) : ℝ

Equations

• QuantumParallelRepetition.universalErrorCeiling K₀ = K₀ * (1 + 2 ^ (1 / 6)) + 2

noncomputable def QuantumParallelRepetition.totalSamplingLoss (K₀ α η lam : ℝ) : ℝ

Equations

• QuantumParallelRepetition.totalSamplingLoss K₀ α η lam = 5 * lam + 2 * (K₀ * (α ^ (1 / 12) + (32 * η) ^ (1 / 12)) + √(8 * η) + QuantumParallelRepetition.universalErrorCeiling K₀ * lam)

noncomputable def QuantumParallelRepetition.roundedWinningLowerBound (ε K₀ α η lam : ℝ) : ℝ

Equations

• QuantumParallelRepetition.roundedWinningLowerBound ε K₀ α η lam = 1 - ε / 2 - QuantumParallelRepetition.totalSamplingLoss K₀ α η lam

theorem QuantumParallelRepetition.totalSamplingLoss_tendsto_zero {ι : Type u_1} {l : Filter ι} (K₀ : ℝ) {α η lam : ι → ℝ} (hα : Filter.Tendsto α l (nhds 0)) (hη : Filter.Tendsto η l (nhds 0)) (hlam : Filter.Tendsto lam l (nhds 0)) : Filter.Tendsto (fun (i : ι) => totalSamplingLoss K₀ (α i) (η i) (lam i)) l (nhds 0)

theorem QuantumParallelRepetition.totalSamplingLoss_eventually_lt {ι : Type u_1} {l : Filter ι} (K₀ : ℝ) {α η lam : ι → ℝ} (hα : Filter.Tendsto α l (nhds 0)) (hη : Filter.Tendsto η l (nhds 0)) (hlam : Filter.Tendsto lam l (nhds 0)) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, totalSamplingLoss K₀ (α i) (η i) (lam i) < ε

theorem QuantumParallelRepetition.source_equation_twenty_nine_contradiction {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : Strategy G) (K₀ α η lam : ℝ) (hbound : roundedWinningLowerBound (1 - entangledValue G) K₀ α η lam ≤ S.winProbability) (herror : totalSamplingLoss K₀ α η lam < (1 - entangledValue G) / 2) : False

theorem QuantumParallelRepetition.matched_payoff_discard_le {ι : Type u_1} [Fintype ι] (weight payoff : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (payoff_le_one : ∀ (i : ι), payoff i ≤ 1) (matched : ι → Bool) : (∑ i : ι, weight i * payoff i - ∑ i : ι, weight i * if matched i = true then 0 else 1) ≤ ∑ i : ι, weight i * if matched i = true then payoff i else 0

theorem QuantumParallelRepetition.squared_state_triangle {E : Type u_1} [NormedAddCommGroup E] (gamma psi phi : E) : ‖gamma - phi‖ ^ 2 ≤ 2 * (‖gamma - psi‖ ^ 2 + ‖psi - phi‖ ^ 2)

theorem QuantumParallelRepetition.source_equation_twenty_one {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] (weight : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (gamma psi phi : ι → E) (η : ℝ) (hgamma : ∑ i : ι, weight i * ‖gamma i - psi i‖ ^ 2 ≤ 8 * η) (hphi : ∑ i : ι, weight i * ‖psi i - phi i‖ ^ 2 ≤ 8 * η) : ∑ i : ι, weight i * ‖gamma i - phi i‖ ^ 2 ≤ 32 * η

theorem QuantumParallelRepetition.weighted_rpow_mean_le {ι : Type u_1} [Fintype ι] (weight value : ι → ℝ) (nonnegative : ∀ (i : ι), 0 ≤ weight i) (normalized : ∑ i : ι, weight i = 1) (value_nonnegative : ∀ (i : ι), 0 ≤ value i) {r : ℝ} (hrzero : 0 ≤ r) (hrone : r ≤ 1) : ∑ i : ι, weight i * value i ^ r ≤ (∑ i : ι, weight i * value i) ^ r

theorem QuantumParallelRepetition.fullHistoryRemaining_insert_conditioned {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) : fullHistoryRemaining n (insert i D) L = fullHistoryRemaining n D (insert i L)

def QuantumParallelRepetition.fullHistoryRemainingInsertedEquiv {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) : ↥(fullHistoryRemaining n (insert i D) L) ≃ ↥(fullHistoryRemaining n D (insert i L))

Equations

• QuantumParallelRepetition.fullHistoryRemainingInsertedEquiv D L i = Equiv.subtypeEquivRight ⋯

def QuantumParallelRepetition.fullCoordinateAnswerExtension {T : Type u_1} {n : ℕ} (D : Finset (Fin n)) (i : Fin n) (α : ↥D → T) (a : T) : ↥(insert i D) → T

Equations

• QuantumParallelRepetition.fullCoordinateAnswerExtension D i α a j = if hj : ↑j = i then a else α ⟨↑j, ⋯⟩

def QuantumParallelRepetition.fullCoordinateAnswerExtensionEquiv {T : Type u_1} [Fintype T] {n : ℕ} (D : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) : (↥D → T) × T ≃ (↥(insert i D) → T)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateInsertedHistory {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) : FullSubsetHistory X Y n (insert i D) L

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateBaseOfInsertedHistory {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (h : FullSubsetHistory X Y n (insert i D) L) : FullCoordinateRevealHistory X Y n D L i

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.fullCoordinateInsertedHistoryEquiv {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) : FullCoordinateRevealHistory X Y n D L i × X × Y ≃ FullSubsetHistory X Y n (insert i D) L

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullCoordinateInsertedHistory_weight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) : fullHistoryWeight G (fullCoordinateInsertedHistory D L i r x y) = fullCoordinateBaseWeight G D L i r * G.questionWeight x y

theorem QuantumParallelRepetition.conditionedAliceEffect_insert_eq_coordinate {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (α : ↥D → A) (a : A) (xs : Fin n → X) : conditionedAliceEffect G n S (insert i D) (fullCoordinateAnswerExtension D i α a) xs = conditionedAliceCoordinateEffect G n S D α xs i a

theorem QuantumParallelRepetition.conditionedBobEffect_insert_eq_coordinate {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (β : ↥D → B) (b : B) (ys : Fin n → Y) : conditionedBobEffect G n S (insert i D) (fullCoordinateAnswerExtension D i β b) ys = conditionedBobCoordinateEffect G n S D β ys i b

theorem QuantumParallelRepetition.conditionedCoordinateEffects_born_expansion {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (α : ↥D → A) (β : ↥D → B) (xs : Fin n → X) (ys : Fin n → Y) (i : Fin n) (a : A) (b : B) : ((bornTracePairing S.state.matrix) (conditionedAliceCoordinateEffect G n S D α xs i a)) (conditionedBobCoordinateEffect G n S D β ys i b) = ∑ aa : Fin n → A, ∑ bb : Fin n → B, if (∀ (j : Fin n) (hj : j ∈ D), aa j = α ⟨j, hj⟩) ∧ aa i = a then if (∀ (j : Fin n) (hj : j ∈ D), bb j = β ⟨j, hj⟩) ∧ bb i = b then S.outcomeProbability xs ys aa bb else 0 else 0

noncomputable def QuantumParallelRepetition.normalizedPureVector {d : Type u_1} [Fintype d] (z : EuclideanSpace ℂ d) : EuclideanSpace ℂ d

Equations

• QuantumParallelRepetition.normalizedPureVector z = ↑‖z‖⁻¹ • z

theorem QuantumParallelRepetition.quadraticExpectation_normalizedPureVector {d : Type u_1} [Fintype d] (W : EuclideanSpace ℂ d →L[ℂ] EuclideanSpace ℂ d) (z : EuclideanSpace ℂ d) : quadraticExpectation W (normalizedPureVector z) = quadraticExpectation W z / ‖z‖ ^ 2

theorem QuantumParallelRepetition.exists_repeatedStrategy_of_lt_entangledValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {r : ℝ} (hr : 0 < r) (hvalue : r < repeatedEntangledValue G n) : ∃ (S : Strategy (G.repeat n)), r < S.winProbability

theorem QuantumParallelRepetition.exists_purifiedRepeatedStrategy_of_lt_entangledValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} {r : ℝ} (hr : 0 < r) (hvalue : r < repeatedEntangledValue G n) : ∃ (S : Strategy (G.repeat n)), r < (purifiedStrategy S).winProbability

theorem QuantumParallelRepetition.arbitrarily_large_purifiedRepeatedStrategy_of_subexponentialWitness {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (hwitness : HasSubexponentialWitness (repeatedEntangledValue G)) {c : ℝ} (hc : 0 < c) (N : ℕ) : ∃ (n : ℕ), N < n ∧ ∃ (S : Strategy (G.repeat n)), Real.exp (-c * ↑n) < (purifiedStrategy S).winProbability

theorem QuantumParallelRepetition.postselection_log_cost_le {θ p : ℝ} (hθ : 0 < θ) (hθp : θ ≤ p) : Real.log (1 / p) ≤ Real.log (1 / θ)

theorem QuantumParallelRepetition.greedy_terminal_of_log_cost {θ η : ℝ} {T : ℕ} (hθ : 0 < θ) (hη_one : η ≤ 1) (hcost : Real.log (1 / θ) < η * ↑T) : (1 - η) ^ T < θ

theorem QuantumParallelRepetition.divisorStopping_nat_bound {n q : ℕ} (hq : 0 < q) (hqn : q ≤ n) : n < 2 * (n / q) * q

theorem QuantumParallelRepetition.sourceRate_mul_lt_divisorStopping {n q : ℕ} (hq : 0 < q) (hqn : q ≤ n) {η : ℝ} (hη : 0 < η) : η / (4 * ↑q) * ↑n < η * ↑(n / q)

theorem QuantumParallelRepetition.repeatedStrategy_exists_divisor_greedy_conditioning {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) {η : ℝ} {q : ℕ} (hη : 0 < η) (hη_one : η ≤ 1) (hq : 0 < q) (hqn : q ≤ n) (hwitness : Real.exp (-(η / (4 * ↑q)) * ↑n) < S.winProbability) : ∃ (D : Finset (Fin n)), D.card < n / q ∧ S.winProbability ≤ (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) ∧ ∑ i ∈ Finset.univ \ D, (strategyEventLaw (G.repeat n) S).failureMass (repeatedCoordinateWin G n) D i < ↑(Finset.univ \ D).card * (η * (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))

theorem QuantumParallelRepetition.divisor_greedy_card_mul_lt {n q : ℕ} (hq : 0 < q) {D : Finset (Fin n)} (hD : D.card < n / q) : D.card * q < n

structure QuantumParallelRepetition.SourceHistoryFlag (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max (max (max u_5 u_6) u_7) u_8)

• permutation : SourceRemainingPermutation D
• position : Fin (Finset.univ \ D).card
• history : FullCoordinateRevealHistory X Y n D (sourceRemainingPermutationPrefix D self.permutation self.position.castSucc) (sourceRemainingPermutationCoordinate D self.permutation self.position)
• aliceAnswer : ↥D → A
• bobAnswer : ↥D → B

@[reducible, inline]

abbrev QuantumParallelRepetition.SourceHistoryFlagTuple (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max (max u_8 u_7) u_6 u_5)

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.sourceHistoryFlagEquiv {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : SourceHistoryFlag X Y A B D ≃ SourceHistoryFlagTuple X Y A B D

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance QuantumParallelRepetition.sourceHistoryFlagFintype {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Fintype (SourceHistoryFlag X Y A B D)

Equations

• QuantumParallelRepetition.sourceHistoryFlagFintype D = Fintype.ofEquiv (QuantumParallelRepetition.SourceHistoryFlagTuple X Y A B D) (QuantumParallelRepetition.sourceHistoryFlagEquiv D).symm

theorem QuantumParallelRepetition.sourceHistoryFlag_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) (f : SourceHistoryFlag X Y A B D → ℝ) : ∑ r : SourceHistoryFlag X Y A B D, f r = ∑ π : SourceRemainingPermutation D, ∑ k : Fin (Finset.univ \ D).card, ∑ r : FullCoordinateRevealHistory X Y n D (sourceRemainingPermutationPrefix D π k.castSucc) (sourceRemainingPermutationCoordinate D π k), ∑ α : ↥D → A, ∑ β : ↥D → B, f { permutation := π, position := k, history := r, aliceAnswer := α, bobAnswer := β }

noncomputable def QuantumParallelRepetition.sourceHistoryPermutationPositionWeight {n : ℕ} (D : Finset (Fin n)) : ℝ

Equations

• QuantumParallelRepetition.sourceHistoryPermutationPositionWeight D = 1 / (↑(Fintype.card (QuantumParallelRepetition.SourceRemainingPermutation D)) * ↑(Finset.univ \ D).card)

noncomputable def QuantumParallelRepetition.sourceHistoryRaw {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (r : SourceHistoryFlag X Y A B D) : ℝ

Equations

• One or more equations did not get rendered due to their size.

def QuantumParallelRepetition.postselectionMass {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : ℝ

Equations

• QuantumParallelRepetition.postselectionMass law wins C = law.eventMass (QuantumParallelRepetition.FiniteEventLaw.winEvent wins C)

theorem QuantumParallelRepetition.allWinMass_le_postselectionMass {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : law.eventMass (FiniteEventLaw.winEvent wins Finset.univ) ≤ postselectionMass law wins C

theorem QuantumParallelRepetition.postselectionMass_le_one {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : postselectionMass law wins C ≤ 1

noncomputable def QuantumParallelRepetition.conditionalCoordinateFailure {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) (i : ι) : ℝ

Equations

• QuantumParallelRepetition.conditionalCoordinateFailure law wins C i = law.failureMass wins C i / QuantumParallelRepetition.postselectionMass law wins C

noncomputable def QuantumParallelRepetition.uniformRemainingFailure {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) : ℝ

Equations

• QuantumParallelRepetition.uniformRemainingFailure law wins C = (∑ i ∈ Finset.univ \ C, QuantumParallelRepetition.conditionalCoordinateFailure law wins C i) / ↑(Finset.univ \ C).card

theorem QuantumParallelRepetition.uniformRemainingFailure_lt_of_failure_sum {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Ω] (law : FiniteEventLaw Ω) (wins : ι → Ω → Bool) (C : Finset ι) {η : ℝ} (hp : 0 < postselectionMass law wins C) (hm : 0 < (Finset.univ \ C).card) (hfailure : ∑ i ∈ Finset.univ \ C, law.failureMass wins C i < ↑(Finset.univ \ C).card * (η * postselectionMass law wins C)) : uniformRemainingFailure law wins C < η

def QuantumParallelRepetition.repeatedPostselectionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (C : Finset (Fin n)) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.repeated_winProbability_le_postselectionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (C : Finset (Fin n)) : S.winProbability ≤ repeatedPostselectionMass G n S C

theorem QuantumParallelRepetition.repeatedPostselectionMass_pos {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (C : Finset (Fin n)) (hwin : 0 < S.winProbability) : 0 < repeatedPostselectionMass G n S C

theorem QuantumParallelRepetition.remainingCoordinates_card {n : ℕ} (C : Finset (Fin n)) : (Finset.univ \ C).card = n - C.card

theorem QuantumParallelRepetition.repeatedStrategy_exists_conditioning {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) {η : ℝ} {q : ℕ} (hwin : 0 < S.winProbability) (hη : 0 < η) (hη_one : η ≤ 1) (hq : q ≤ n) (hterminal : (1 - η) ^ q < S.winProbability) : ∃ (C : Finset (Fin n)), C.card < q ∧ S.winProbability ≤ repeatedPostselectionMass G n S C ∧ 0 < repeatedPostselectionMass G n S C ∧ 0 < (Finset.univ \ C).card ∧ uniformRemainingFailure (strategyEventLaw (G.repeat n) S) (repeatedCoordinateWin G n) C < η

theorem QuantumParallelRepetition.source_equation_nineteen_alice {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : -((bornTracePairing ρ.matrix) (cfc (fun (z : ℝ) => z * Real.log z) F)) G ≤ (((bornTracePairing ρ.matrix) F) G).negMulLog

theorem QuantumParallelRepetition.source_equation_nineteen_bob {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] [DecidableEq dA] [DecidableEq dB] (ρ : DensityMatrix (dA × dB)) (F : Matrix dA dA ℂ) (hF : F.PosSemidef) (hFcomplement : (1 - F).PosSemidef) (G : Matrix dB dB ℂ) (hG : G.PosSemidef) (hGcomplement : (1 - G).PosSemidef) : -((bornTracePairing ρ.matrix) F) (cfc (fun (z : ℝ) => z * Real.log z) G) ≤ (((bornTracePairing ρ.matrix) F) G).negMulLog

noncomputable def QuantumParallelRepetition.postselectionLogCost {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

Equations

• QuantumParallelRepetition.postselectionLogCost G n S D = Real.log (1 / QuantumParallelRepetition.repeatedPostselectionMass G n S D)

noncomputable def QuantumParallelRepetition.answerLogCost {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ℝ

Equations

• QuantumParallelRepetition.answerLogCost D = ↑D.card * Real.log (↑(Fintype.card A) * ↑(Fintype.card B))

noncomputable def QuantumParallelRepetition.martingaleRate {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

Equations

• QuantumParallelRepetition.martingaleRate G n S D = (QuantumParallelRepetition.postselectionLogCost G n S D + QuantumParallelRepetition.answerLogCost D) / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.answerCount_pos_of_postselection {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : 0 < fullHistoryAnswerCount D

theorem QuantumParallelRepetition.martingale_log_cost_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : Real.log (fullHistoryAnswerCount D / repeatedPostselectionMass G n S D) = postselectionLogCost G n S D + answerLogCost D

theorem QuantumParallelRepetition.aliceMartingaleEntropyBudget {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) (hp : 0 < repeatedPostselectionMass G n S D) : sourceUniformPermutationAverage D (sourcePermutationAliceEntropyIncrement G n S D) ≤ repeatedPostselectionMass G n S D * martingaleRate G n S D

theorem QuantumParallelRepetition.bornWeighted_normalized_distance {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] (fallback u v : E) (hfallback : ‖fallback‖ = 1) : ‖u‖ ^ 2 * ‖normalizeOrDefault fallback u - normalizeOrDefault fallback v‖ ^ 2 ≤ 4 * ‖u - v‖ ^ 2

theorem QuantumParallelRepetition.fullCoordinateInsertedHistory_winIndicator_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (α : ↥D → A) (a : A) (β : ↥D → B) (b : B) : fullHistoryWinIndicator G (fullCoordinateInsertedHistory D L i r x y) (fullCoordinateAnswerExtension D i α a) (fullCoordinateAnswerExtension D i β b) = fullCoordinateBaseWinIndicator G D L i r α β * if G.predicate x y a b = true then 1 else 0

def QuantumParallelRepetition.fullCoordinateInsertedHiddenAliceEquiv {X : Type u_5} {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) : (↥(fullHistoryRemaining n (insert i D) L) → X) ≃ (↥(fullHistoryRemaining n D (insert i L)) → X)

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullCoordinateInsertedAliceQuestion_eq {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥(fullHistoryRemaining n D (insert i L)) → X) : fullHistoryAliceQuestion (fullCoordinateInsertedHistory D L i r x y) ((fullCoordinateInsertedHiddenAliceEquiv D L i).symm hidden) = fullHistoryAliceQuestion (fullCoordinateNewHistory D L i r x) hidden

theorem QuantumParallelRepetition.fullCoordinateInsertedHiddenAliceWeight_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥(fullHistoryRemaining n D (insert i L)) → X) : fullHistoryHiddenAliceWeight G (fullCoordinateInsertedHistory D L i r x y) ((fullCoordinateInsertedHiddenAliceEquiv D L i).symm hidden) = fullHistoryHiddenAliceWeight G (fullCoordinateNewHistory D L i r x) hidden

theorem QuantumParallelRepetition.fullCoordinateInsertedBobQuestion_eq {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥L → Y) : fullHistoryBobQuestion (fullCoordinateInsertedHistory D L i r x y) hidden = fullHistoryBobQuestion (fullCoordinateOldHistory D L i r y) hidden

theorem QuantumParallelRepetition.fullCoordinateInsertedHiddenBobWeight_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (hidden : ↥L → Y) : fullHistoryHiddenBobWeight G (fullCoordinateInsertedHistory D L i r x y) hidden = fullHistoryHiddenBobWeight G (fullCoordinateOldHistory D L i r y) hidden

theorem QuantumParallelRepetition.fullCoordinateInsertedHistory_aliceFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (α : ↥D → A) (a : A) : fullHistoryAliceFilter G n S (insert i D) L (fullCoordinateInsertedHistory D L i r x y) (fullCoordinateAnswerExtension D i α a) = fullCoordinateAliceRefinementEffect G n S D L i r α x a

theorem QuantumParallelRepetition.fullCoordinateInsertedHistory_bobFilter {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (r : FullCoordinateRevealHistory X Y n D L i) (x : X) (y : Y) (β : ↥D → B) (b : B) : fullHistoryBobFilter G n S (insert i D) L (fullCoordinateInsertedHistory D L i r x y) (fullCoordinateAnswerExtension D i β b) = fullCoordinateBobRefinementEffect G n S D L i r β y b

theorem QuantumParallelRepetition.fullCoordinateInsertedHistory_sum {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] {T : Type u_5} [AddCommMonoid T] {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (f : FullSubsetHistory X Y n (insert i D) L → T) : ∑ h : FullSubsetHistory X Y n (insert i D) L, f h = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ x : X, ∑ y : Y, f (fullCoordinateInsertedHistory D L i r x y)

theorem QuantumParallelRepetition.fullCoordinateAnswerExtension_sum {T : Type u_5} {R : Type u_6} [Fintype T] [AddCommMonoid R] {n : ℕ} (D : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (f : (↥(insert i D) → T) → R) : ∑ α : ↥(insert i D) → T, f α = ∑ α : ↥D → T, ∑ a : T, f (fullCoordinateAnswerExtension D i α a)

theorem QuantumParallelRepetition.fullCoordinateWeightedInsertedSum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (value : FullSubsetHistory X Y n (insert i D) L → (↥(insert i D) → A) → (↥(insert i D) → B) → ℝ) : ∑ h : FullSubsetHistory X Y n (insert i D) L, ∑ α : ↥(insert i D) → A, ∑ β : ↥(insert i D) → B, fullHistoryWeight G h * fullHistoryWinIndicator G h α β * value h α β = ∑ r : FullCoordinateRevealHistory X Y n D L i, ∑ α : ↥D → A, ∑ β : ↥D → B, fullCoordinateBaseWeight G D L i r * fullCoordinateBaseWinIndicator G D L i r α β * ∑ x : X, ∑ y : Y, G.questionWeight x y * ∑ a : A, ∑ b : B, (if G.predicate x y a b = true then 1 else 0) * value (fullCoordinateInsertedHistory D L i r x y) (fullCoordinateAnswerExtension D i α a) (fullCoordinateAnswerExtension D i β b)

noncomputable def QuantumParallelRepetition.fullCoordinateAcceptedPostselectedMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.fullCoordinateAcceptedPostselectedMass_eq {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D L : Finset (Fin n)) (i : Fin n) (hiD : i ∉ D) (hiL : i ∉ L) (hL : L ⊆ Finset.univ \ D) : fullCoordinateAcceptedPostselectedMass G n S D L i = (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) (insert i D))

noncomputable def QuantumParallelRepetition.sourceHistoryAcceptedQuestionMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (r : SourceHistoryFlag X Y A B D) (x : X) (y : Y) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuantumParallelRepetition.sourceHistoryAcceptedMass {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.sourceHistoryQuadraticExpectation_matrix_sum {I : Type u_5} {d : Type u_6} [Fintype I] [Fintype d] [DecidableEq d] (M : I → Matrix d d ℂ) (z : EuclideanSpace ℂ d) : quadraticExpectation (Matrix.toEuclideanCLM (∑ i : I, M i)) z = ∑ i : I, quadraticExpectation (Matrix.toEuclideanCLM (M i)) z

theorem QuantumParallelRepetition.sourceHistoryAcceptedMass_eq_uniform {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : sourceHistoryAcceptedMass G n S D = sourceUniformPermutationAverage D fun (π : SourceRemainingPermutation D) (k : Fin (Finset.univ \ D).card) => (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) (insert (sourceRemainingPermutationCoordinate D π k) D))

theorem QuantumParallelRepetition.sourceHistoryAcceptedMass_eq_remaining_average {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : sourceHistoryAcceptedMass G n S D = (∑ i : SourceRemainingCoordinate D, (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) (insert (↑i) D))) / ↑(Finset.univ \ D).card

theorem QuantumParallelRepetition.sourceHistoryAcceptedMass_gt_of_greedy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) {η : ℝ} (hgreedy : ∑ i ∈ Finset.univ \ D, (strategyEventLaw (G.repeat n) S).failureMass (repeatedCoordinateWin G n) D i < ↑(Finset.univ \ D).card * (η * (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D))) : (1 - η) * (strategyEventLaw (G.repeat n) S).eventMass (FiniteEventLaw.winEvent (repeatedCoordinateWin G n) D) < sourceHistoryAcceptedMass G n S D

noncomputable def QuantumParallelRepetition.taggedTensorVector {R : Type u_1} {ι : R → Type u_2} (r : R) (z : EuclideanSpace ℂ (ι r × ι r)) : EuclideanSpace ℂ ((PUnit.{1} ⊕ (r : R) × ι r) × (PUnit.{1} ⊕ (r : R) × ι r))

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.taggedTensorVector_norm {R : Type u_1} [Fintype R] {ι : R → Type u_2} [(r : R) → Fintype (ι r)] (r : R) (z : EuclideanSpace ℂ (ι r × ι r)) : ‖taggedTensorVector r z‖ = ‖z‖

theorem QuantumParallelRepetition.taggedTensorVector_sub {R : Type u_1} {ι : R → Type u_2} (r : R) (u v : EuclideanSpace ℂ (ι r × ι r)) : taggedTensorVector r (u - v) = taggedTensorVector r u - taggedTensorVector r v

theorem QuantumParallelRepetition.martingaleRate_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) (hp : 0 < repeatedPostselectionMass G n S D) : 0 ≤ martingaleRate G n S D

theorem QuantumParallelRepetition.remainingCoordinate_card_pos {n : ℕ} (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) : 0 < Fintype.card (SourceRemainingCoordinate D)

theorem QuantumParallelRepetition.finiteTotalVariation_triangle {ι : Type u_5} [Fintype ι] (p q r : ι → ℝ) : Pinsker.finiteTotalVariation p r ≤ Pinsker.finiteTotalVariation p q + Pinsker.finiteTotalVariation q r

def QuantumParallelRepetition.weightedConditionalJoint {κ : Type u_5} {ι : Type u_6} [Fintype κ] [Fintype ι] (weight : κ → ℝ) (conditional : κ → ι → ℝ) : κ × ι → ℝ

Equations

• QuantumParallelRepetition.weightedConditionalJoint weight conditional t = weight t.1 * conditional t.1 t.2

theorem QuantumParallelRepetition.weightedConditionalJoint_totalVariation {κ : Type u_5} {ι : Type u_6} [Fintype κ] [Fintype ι] (weight : κ → ℝ) (hweight : ∀ (k : κ), 0 ≤ weight k) (left right : κ → ι → ℝ) : Pinsker.finiteTotalVariation (weightedConditionalJoint weight left) (weightedConditionalJoint weight right) = ∑ k : κ, weight k * Pinsker.finiteTotalVariation (left k) (right k)

theorem QuantumParallelRepetition.finiteTotalVariation_equiv {ι : Type u_5} {κ : Type u_6} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (p q : κ → ℝ) : Pinsker.finiteTotalVariation (p ∘ ⇑e) (q ∘ ⇑e) = Pinsker.finiteTotalVariation p q

@[reducible, inline]

abbrev QuantumParallelRepetition.LocalQuestionContext (X : Type u_5) (Y : Type u_6) [Fintype X] [Fintype Y] {n : ℕ} (D : Finset (Fin n)) : Type (max u_6 u_5)

Equations

• QuantumParallelRepetition.LocalQuestionContext X Y D = (QuantumParallelRepetition.SourceRemainingCoordinate D × X × Y)

noncomputable def QuantumParallelRepetition.localQuestionWeight {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (c : LocalQuestionContext X Y D) : ℝ

Equations

• QuantumParallelRepetition.localQuestionWeight G n D c = G.questionWeight c.2.1 c.2.2 / ↑(Fintype.card (QuantumParallelRepetition.SourceRemainingCoordinate D))

theorem QuantumParallelRepetition.localQuestionWeight_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (c : LocalQuestionContext X Y D) : 0 ≤ localQuestionWeight G n D c

theorem QuantumParallelRepetition.localQuestionWeight_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (D : Finset (Fin n)) (hm : 0 < (Finset.univ \ D).card) : ∑ c : LocalQuestionContext X Y D, localQuestionWeight G n D c = 1

noncomputable def QuantumParallelRepetition.conditionedEventDistribution {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) : Ω → ℝ

Equations

• QuantumParallelRepetition.conditionedEventDistribution law event ω = if ω ∈ event then law.weight ω / law.eventMass event else 0

theorem QuantumParallelRepetition.conditionedEventDistribution_nonneg {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) (ω : Ω) : 0 ≤ conditionedEventDistribution law event ω

theorem QuantumParallelRepetition.conditionedEventDistribution_sum {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) : ∑ ω : Ω, conditionedEventDistribution law event ω = 1

theorem QuantumParallelRepetition.conditionedEventDistribution_absolute_continuity {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (ω : Ω) : law.weight ω = 0 → conditionedEventDistribution law event ω = 0

theorem QuantumParallelRepetition.conditionedEventDistribution_relativeEntropy {Ω : Type u_5} [Fintype Ω] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) : Pinsker.finiteRelativeEntropy (conditionedEventDistribution law event) law.weight = Real.log (1 / law.eventMass event)

theorem QuantumParallelRepetition.conditionedEventDistribution_projection_relativeEntropy_le {Ω : Type u_5} {κ : Type u_6} [Fintype Ω] [Fintype κ] (law : FiniteEventLaw Ω) (event : Finset Ω) (positive : 0 < law.eventMass event) (projection : Ω → κ) : Pinsker.finiteRelativeEntropy (ClassicalInformation.groupedMass projection (conditionedEventDistribution law event)) (ClassicalInformation.groupedMass projection law.weight) ≤ Real.log (1 / law.eventMass event)

noncomputable def QuantumParallelRepetition.repeatedConditionedOutcomeLaw {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) : StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B) → ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.repeatedConditionedOutcomeLaw_relativeEntropy {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : Pinsker.finiteRelativeEntropy (repeatedConditionedOutcomeLaw G n S D) (strategyEventLaw (G.repeat n) S).weight = postselectionLogCost G n S D

noncomputable def QuantumParallelRepetition.finiteUniformWeight (Z : Type u_1) [Fintype Z] : ℝ

Equations

• QuantumParallelRepetition.finiteUniformWeight Z = 1 / ↑(Fintype.card Z)

theorem QuantumParallelRepetition.finiteUniformWeight_pos {Z : Type u_1} [Fintype Z] (positive : 0 < Fintype.card Z) : 0 < finiteUniformWeight Z

theorem QuantumParallelRepetition.finiteUniformWeight_sum {Z : Type u_1} [Fintype Z] (positive : 0 < Fintype.card Z) : ∑ _z : Z, finiteUniformWeight Z = 1

theorem QuantumParallelRepetition.finiteProbability_le_one {Z : Type u_1} [Fintype Z] (p : Z → ℝ) (nonnegative : ∀ (z : Z), 0 ≤ p z) (normalized : ∑ z : Z, p z = 1) (z : Z) : p z ≤ 1

theorem QuantumParallelRepetition.finiteRelativeEntropy_uniform_le_log_card {Z : Type u_1} [Fintype Z] (p : Z → ℝ) (nonnegative : ∀ (z : Z), 0 ≤ p z) (normalized : ∑ z : Z, p z = 1) (positive : 0 < Fintype.card Z) : (Pinsker.finiteRelativeEntropy p fun (x : Z) => finiteUniformWeight Z) ≤ Real.log ↑(Fintype.card Z)

noncomputable def QuantumParallelRepetition.uniformFlagReference {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (prior : Ω → ℝ) : Ω × Z → ℝ

Equations

• QuantumParallelRepetition.uniformFlagReference prior t = prior t.1 * QuantumParallelRepetition.finiteUniformWeight Z

theorem QuantumParallelRepetition.uniformFlagReference_nonneg {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (prior : Ω → ℝ) (nonnegative : ∀ (ω : Ω), 0 ≤ prior ω) (positive : 0 < Fintype.card Z) (t : Ω × Z) : 0 ≤ uniformFlagReference prior t

theorem QuantumParallelRepetition.uniformFlagReference_sum {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (prior : Ω → ℝ) (normalized : ∑ ω : Ω, prior ω = 1) (positive : 0 < Fintype.card Z) : ∑ t : Ω × Z, uniformFlagReference prior t = 1

theorem QuantumParallelRepetition.uniformFlagReference_firstMarginal {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (prior : Ω → ℝ) (positive : 0 < Fintype.card Z) : ClassicalInformation.jointFirstMarginal (uniformFlagReference prior) = prior

theorem QuantumParallelRepetition.uniformFlagReference_conditional {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (prior : Ω → ℝ) (positive : 0 < Fintype.card Z) (ω : Ω) (hprior : prior ω ≠ 0) : ClassicalInformation.jointConditional (uniformFlagReference prior) ω = fun (x : Z) => finiteUniformWeight Z

theorem QuantumParallelRepetition.uniformFlagReference_absolute_continuity {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (joint : Ω × Z → ℝ) (prior : Ω → ℝ) (hjoint : ∀ (t : Ω × Z), 0 ≤ joint t) (absolute_continuity : ∀ (ω : Ω), prior ω = 0 → ClassicalInformation.jointFirstMarginal joint ω = 0) (positive : 0 < Fintype.card Z) (t : Ω × Z) : uniformFlagReference prior t = 0 → joint t = 0

theorem QuantumParallelRepetition.uniformFlagRelativeEntropy_le {Ω : Type u_1} {Z : Type u_2} [Fintype Ω] [Fintype Z] (joint : Ω × Z → ℝ) (prior : Ω → ℝ) (hjoint : ∀ (t : Ω × Z), 0 ≤ joint t) (hprior : ∀ (ω : Ω), 0 ≤ prior ω) (joint_normalized : ∑ t : Ω × Z, joint t = 1) (prior_normalized : ∑ ω : Ω, prior ω = 1) (absolute_continuity : ∀ (ω : Ω), prior ω = 0 → ClassicalInformation.jointFirstMarginal joint ω = 0) (positive : 0 < Fintype.card Z) : Pinsker.finiteRelativeEntropy joint (uniformFlagReference prior) ≤ Pinsker.finiteRelativeEntropy (ClassicalInformation.jointFirstMarginal joint) prior + Real.log ↑(Fintype.card Z)

theorem QuantumParallelRepetition.finiteRelativeEntropy_nonneg {Ω : Type u_1} [Fintype Ω] (p q : Ω → ℝ) (hp : ∀ (ω : Ω), 0 ≤ p ω) (hq : ∀ (ω : Ω), 0 ≤ q ω) : 0 ≤ Pinsker.finiteRelativeEntropy p q

theorem QuantumParallelRepetition.groupedMass_nonneg {Ω : Type u_1} {κ : Type u_2} [Fintype Ω] [Fintype κ] [DecidableEq κ] (f : Ω → κ) (p : Ω → ℝ) (hp : ∀ (ω : Ω), 0 ≤ p ω) (a : κ) : 0 ≤ ClassicalInformation.groupedMass f p a

theorem QuantumParallelRepetition.groupedMass_absolute_continuity {Ω : Type u_1} {κ : Type u_2} [Fintype Ω] [Fintype κ] [DecidableEq κ] (f : Ω → κ) (p q : Ω → ℝ) (hq : ∀ (ω : Ω), 0 ≤ q ω) (absolute_continuity : ∀ (ω : Ω), q ω = 0 → p ω = 0) (a : κ) : ClassicalInformation.groupedMass f q a = 0 → ClassicalInformation.groupedMass f p a = 0

theorem QuantumParallelRepetition.groupedMass_comp {Ω : Type u_1} {κ : Type u_2} {θ : Type u_3} [Fintype Ω] [Fintype κ] [Fintype θ] [DecidableEq κ] [DecidableEq θ] (f : Ω → κ) (g : κ → θ) (p : Ω → ℝ) : ClassicalInformation.groupedMass g (ClassicalInformation.groupedMass f p) = ClassicalInformation.groupedMass (g ∘ f) p

theorem QuantumParallelRepetition.groupedMass_id {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (p : Ω → ℝ) : ClassicalInformation.groupedMass id p = p

def QuantumParallelRepetition.finitePrefixMask {Ω : Type u_1} {Y : Type u_2} {h : ℕ} (base : Y) (k : Fin (h + 1)) : Ω × (Fin h → Y) → Ω × (Fin h → Y)

Equations

• QuantumParallelRepetition.finitePrefixMask base k t = (t.1, fun (j : Fin h) => if ↑j < ↑k then t.2 j else base)

theorem QuantumParallelRepetition.finitePrefixMask_comp {Ω : Type u_1} {Y : Type u_2} {h : ℕ} (base : Y) (k : Fin h) : finitePrefixMask base k.castSucc ∘ finitePrefixMask base k.succ = finitePrefixMask base k.castSucc

theorem QuantumParallelRepetition.finitePrefixMask_last {Ω : Type u_1} {Y : Type u_2} {h : ℕ} (base : Y) : finitePrefixMask base (Fin.last h) = id

noncomputable def QuantumParallelRepetition.finitePrefixRelativeEntropy {Ω : Type u_1} {Y : Type u_2} [Fintype Ω] [Fintype Y] {h : ℕ} (joint prior : Ω × (Fin h → Y) → ℝ) (base : Y) (k : Fin (h + 1)) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.finitePrefixRelativeEntropy_telescope {Ω : Type u_1} {Y : Type u_2} [Fintype Ω] [Fintype Y] {h : ℕ} (joint prior : Ω × (Fin h → Y) → ℝ) (base : Y) : ∑ k : Fin h, (finitePrefixRelativeEntropy joint prior base k.succ - finitePrefixRelativeEntropy joint prior base k.castSucc) = Pinsker.finiteRelativeEntropy joint prior - finitePrefixRelativeEntropy joint prior base 0

theorem QuantumParallelRepetition.finitePrefixRelativeEntropy_budget {Ω : Type u_1} {Y : Type u_2} [Fintype Ω] [Fintype Y] {h : ℕ} (joint prior : Ω × (Fin h → Y) → ℝ) (hjoint : ∀ (t : Ω × (Fin h → Y)), 0 ≤ joint t) (hprior : ∀ (t : Ω × (Fin h → Y)), 0 ≤ prior t) (base : Y) : ∑ k : Fin h, (finitePrefixRelativeEntropy joint prior base k.succ - finitePrefixRelativeEntropy joint prior base k.castSucc) ≤ Pinsker.finiteRelativeEntropy joint prior

theorem QuantumParallelRepetition.reversePartition_relativeEntropy_budget {M : Type u_1} [Fintype M] [DecidableEq M] (nonempty : 0 < Fintype.card M) (increment : (s : Finset M) → Fin s.card → ℝ) {cost : ℝ} (hcost : 0 ≤ cost) (hbudget : ∀ (s : Finset M), ∑ k : Fin s.card, increment s k ≤ cost) : ∑ s : Finset M, reversePartitionWeight s * ((∑ k : Fin s.card, increment s k) / ↑s.card) ≤ 2 * cost / ↑(Fintype.card M)

theorem QuantumParallelRepetition.groupedMass_sum {Ω : Type u_5} {κ : Type u_6} [Fintype Ω] [Fintype κ] [DecidableEq κ] (projection : Ω → κ) (mass : Ω → ℝ) : ∑ a : κ, ClassicalInformation.groupedMass projection mass a = ∑ ω : Ω, mass ω

theorem QuantumParallelRepetition.groupedMass_first {Ω : Type u_5} {Z : Type u_6} [Fintype Ω] [Fintype Z] [DecidableEq Ω] (joint : Ω × Z → ℝ) : ClassicalInformation.groupedMass Prod.fst joint = ClassicalInformation.jointFirstMarginal joint

@[reducible, inline]

abbrev QuantumParallelRepetition.ConditionedAnswerFlag (A : Type u_5) (B : Type u_6) [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : Type (max u_5 u_6)

Equations

• QuantumParallelRepetition.ConditionedAnswerFlag A B D = ((↥D → A) × (↥D → B))

def QuantumParallelRepetition.repeatedConditionedAnswerFlag {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (_S : Strategy (G.repeat n)) (D : Finset (Fin n)) (ω : StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) : ConditionedAnswerFlag A B D

Equations

• QuantumParallelRepetition.repeatedConditionedAnswerFlag G n _S D ω = (fun (i : ↥D) => ω.2.2.1 ↑i, fun (i : ↥D) => ω.2.2.2 ↑i)

theorem QuantumParallelRepetition.conditionedAnswerFlag_card {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {n : ℕ} (D : Finset (Fin n)) : ↑(Fintype.card (ConditionedAnswerFlag A B D)) = fullHistoryAnswerCount D

theorem QuantumParallelRepetition.conditionedAnswerFlag_card_pos {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : 0 < Fintype.card (ConditionedAnswerFlag A B D)

theorem QuantumParallelRepetition.conditionedAnswerFlag_log_card {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (hp : 0 < repeatedPostselectionMass G n S D) : Real.log ↑(Fintype.card (ConditionedAnswerFlag A B D)) = answerLogCost D

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactOutcome (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) (n : ℕ) : Type (max u_5 (max u_8 u_7) u_6)

Equations

• QuantumParallelRepetition.ExactOutcome X Y A B n = QuantumParallelRepetition.StrategyOutcome (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)

@[reducible, inline]

abbrev QuantumParallelRepetition.ExactJointOutcome (X : Type u_5) (Y : Type u_6) (A : Type u_7) (B : Type u_8) {n : ℕ} (D : Finset (Fin n)) : Type (max (max (max u_8 u_7) u_6) u_5)

Equations

• QuantumParallelRepetition.ExactJointOutcome X Y A B D = (QuantumParallelRepetition.ExactRemainingSeed D × QuantumParallelRepetition.ExactOutcome X Y A B n)

theorem QuantumParallelRepetition.exactRemainingSeedWeight_sum {n : ℕ} (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) : ∑ seed : ExactRemainingSeed D, exactSeedWeight seed = 1

noncomputable def QuantumParallelRepetition.exactPostselectedJointLaw {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (q : ExactJointOutcome X Y A B D) : ℝ

Equations

• QuantumParallelRepetition.exactPostselectedJointLaw G n S D q = QuantumParallelRepetition.exactSeedWeight q.1 * QuantumParallelRepetition.repeatedConditionedOutcomeLaw G n S D q.2

theorem QuantumParallelRepetition.exactPostselectedJointLaw_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (q : ExactJointOutcome X Y A B D) : 0 ≤ exactPostselectedJointLaw G n S D q

theorem QuantumParallelRepetition.exactPostselectedJointLaw_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) : ∑ q : ExactJointOutcome X Y A B D, exactPostselectedJointLaw G n S D q = 1

noncomputable def QuantumParallelRepetition.exactSourcePushforward {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} [Fintype K] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (projection : ExactJointOutcome X Y A B D → K) : K → ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumParallelRepetition.exactSourcePushforward_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} [Fintype K] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (positive : 0 < repeatedPostselectionMass G n S D) (projection : ExactJointOutcome X Y A B D → K) (k : K) : 0 ≤ exactSourcePushforward G n S D projection k

theorem QuantumParallelRepetition.exactSourcePushforward_sum {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {K : Type u_5} [Fintype K] (G : Game X Y A B) (n : ℕ) (S : Strategy (G.repeat n)) (D : Finset (Fin n)) (remaining : 0 < (Finset.univ \ D).card) (positive : 0 < repeatedPostselectionMass G n S D) (projection : ExactJointOutcome X Y A B D → K) : ∑ k : K, exactSourcePushforward G n S D projection k = 1