OAI/Probability/InvariantIsing/Fields/SpinPriorFieldRecursion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the unused tensor marks from the field recursion preserves any finite probability spin prior.

  1. lemma OAI.InvariantIsing.tensorEnergyMarkLaw_zero_amplitude line 13
  2. lemma OAI.InvariantIsing.spinPriorCascadeValue_field line 29
  3. lemma OAI.InvariantIsing.spinPriorFlatLog_field_integral line 52