OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkFibreGiantApproximationMixedDefs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.mixedScalar line 30
  2. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.correctedMixedScalar line 37
  3. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.mixedResidueTest line 44
  4. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.extractedDensity line 54
  5. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.mixedBlockAverage line 58
  6. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.periodicMixed line 77
  7. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.principalMixed line 84
  8. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.sourceMeanMixed line 91
  9. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.periodicCorrectedMixed line 100
  10. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.principalCorrectedMixed line 107
  11. def OAI.Ostmann.Arithmetic.HistoryBulkFibreGiantApproximation.Frame.sourceMeanCorrectedMixed line 114