OAI/Probability/InvariantIsing/Cavity/CavityConcreteComplement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The measurable special frame used in the actual base interaction. Its Gram and cavity-orthogonality identities hold for every input frame.

  1. lemma OAI.InvariantIsing.cavityCompressionGrams_sum line 15
  2. def OAI.InvariantIsing.cavityConcreteComplement line 22
  3. lemma OAI.InvariantIsing.measurable_cavityConcreteComplement line 27
  4. lemma OAI.InvariantIsing.cavityReindexedStack_compression_gram line 35
  5. lemma OAI.InvariantIsing.cavityConcreteComplement_gram line 56
  6. lemma OAI.InvariantIsing.cavityConcreteComplement_perp line 71