OAI/RepresentationTheory/RowColumn/LineStates.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RowColumn.Postselection.allocationPerm line 14
  2. lemma OAI.RowColumn.Postselection.allocationPerm_spec line 18
  3. lemma OAI.RowColumn.Postselection.counts_precomp line 23
  4. def OAI.RowColumn.Postselection.symExtension line 32
  5. lemma OAI.RowColumn.Postselection.symExtension_on_line line 38
  6. lemma OAI.RowColumn.Postselection.symExtension_invariant line 46
  7. lemma OAI.RowColumn.Postselection.symExtension_counts line 72
  8. abbrev OAI.RowColumn.Postselection.Allocations line 80
  9. def OAI.RowColumn.Postselection.labelWordEquiv line 82
  10. def OAI.RowColumn.Postselection.precompWordEquiv line 88
  11. lemma OAI.RowColumn.Postselection.symExtension_norm line 95
  12. def OAI.RowColumn.Postselection.labelTest line 112
  13. lemma OAI.RowColumn.Postselection.labeled_pair line 116
  14. lemma OAI.RowColumn.Postselection.allocation_probability line 125
  15. def OAI.RowColumn.Postselection.lineMass line 144
  16. def OAI.RowColumn.Postselection.normalizedLine line 145
  17. lemma OAI.RowColumn.Postselection.lineMass_nonneg line 149
  18. lemma OAI.RowColumn.Postselection.lineMass_zero line 153
  19. lemma OAI.RowColumn.Postselection.line_reconstruction line 160
  20. lemma OAI.RowColumn.Postselection.normalizedLine_norm line 169
  21. lemma OAI.RowColumn.Postselection.labeled_tensor_pair line 180
  22. lemma OAI.RowColumn.Postselection.symExtension_supported line 198
  23. def OAI.RowColumn.Postselection.lineAmplitude line 211
  24. lemma OAI.RowColumn.Postselection.lineAmplitude_norm line 218
  25. lemma OAI.RowColumn.Postselection.lineAmplitude_support line 224
  26. theorem OAI.RowColumn.Postselection.line_symmetric_postselection line 231

    Source documentation

    Independent fibre postselection, with the allocation factorial cancelled by the exact multinomial probability rather than included in the overhead.

    theorem line_symmetric_postselection (line : S → L) (a₀ : S → A) (hn : 0 < Fintype.card S)
    (good : A → Prop) [DecidablePred good] (v x : (S → A) → ℂ)
    (hv : ∀ p : Equiv.Perm S, (∀ i, line (p i)=line i) → ∀ w, v (w ∘ p)=v w)
    (hsupp : ∀ w, ¬ (∀ i, good (w i)) → v w=0) :
    Complex.normSq (∑ w, v w*x w) ≤
      (∑ w, Complex.normSq (v w)) *
      (((Fintype.card S+1)^(Fintype.card (L × A)) : ℕ) /
        (Fintype.card (Phases (L × A) (Fintype.card S)) : ℝ) *
      ∑ q : Types (S := S) (A := L × A), ∑ θ : Phases (L × A) (Fintype.card S),
…

    Mentions: OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.Types

  27. def OAI.RowColumn.Postselection.lineState line 289
  28. lemma OAI.RowColumn.Postselection.lineState_positive line 295
  29. lemma OAI.RowColumn.Postselection.lineState_trace line 301
  30. lemma OAI.RowColumn.Postselection.lineState_even line 308
  31. lemma OAI.RowColumn.Postselection.variable_purification_pair line 314
  32. lemma OAI.RowColumn.Postselection.variable_purification_quadratic line 319
  33. theorem OAI.RowColumn.Postselection.positive_line_postselection line 331

    Source documentation

    Explicit local domination for independent row/column permutation fibres. All mixture terms are genuine even positive identical-slot substates within each fibre, irrespective of its size and the deletion layout.

    theorem positive_line_postselection (line : S → L) (a₀ : S → C × C) (hn : 0 < Fintype.card S)
    (odd : C → Prop) [DecidablePred odd] (A : Matrix (S → C) (S → C) ℂ)
    (hA : A.PosSemidef)
    (hinv : ∀ (p : Equiv.Perm S), (∀ i, line (p i)=line i) → ∀ (w v : S → C),
      A (w ∘ p) (v ∘ p)=A w v)
    (hsupp : ∀ w v, ¬ (∀ i, odd (w i) ↔ odd (v i)) → A w v=0)
    (x : (S → C) → ℂ) :
    quadratic A x ≤ A.trace.re *
      (((Fintype.card S+1)^(Fintype.card (L × (C × C))) : ℕ) /
        (Fintype.card (Phases (L × (C × C)) (Fintype.card S)) : ℝ) *
      ∑ q : Types (S := S) (A := L × (C × C)),
…

    Mentions: OAI.RowColumn.Postselection.Phases, OAI.RowColumn.Postselection.Types