OAI/NumberTheory/Ostmann/Construction/InitialMovingLogCorrelation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal half-cutoff correlation under the original regular law

  1. theorem OAI.Ostmann.movingTemplate_initial_log_correlation_eq line 11