OAI/NumberTheory/Ostmann/Construction/FixedPivotHYEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sharp history energy under the literal H and Y prime priors

  1. theorem OAI.Ostmann.constituent_fixedPivot_HY_square_rate line 11