OAI/Analysis/ModularRecovery/Model.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Nondegenerate spectral calculus, the closed Tomita graph, and bounded recovery.

  1. def OAI.BoundedRecovery.spectralCharacter line 18

    Also declared: ComparatorChallenges/BoundedRecovery.lean:18 (same declaration text).

  2. def OAI.BoundedRecovery.halfExponentialCutoff line 23

    Also declared: ComparatorChallenges/BoundedRecovery.lean:23 (same declaration text).

  3. structure OAI.BoundedRecovery.RealSpectralCalculus line 31

    Also declared: ComparatorChallenges/BoundedRecovery.lean:31 (same declaration text).

  4. def OAI.BoundedRecovery.RealSpectralCalculus.unitary line 39

    Also declared: ComparatorChallenges/BoundedRecovery.lean:39 (same declaration text).

  5. def OAI.BoundedRecovery.RealSpectralCalculus.halfGraph line 42

    Also declared: ComparatorChallenges/BoundedRecovery.lean:42 (same declaration text).

  6. def OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport line 45

    Also declared: ComparatorChallenges/BoundedRecovery.lean:45 (same declaration text).

  7. structure OAI.BoundedRecovery.StandardModularData line 50

    Also declared: ComparatorChallenges/BoundedRecovery.lean:50 (same declaration text).

  8. def OAI.BoundedRecovery.StandardModularData.sigma line 66

    Also declared: ComparatorChallenges/BoundedRecovery.lean:66 (same declaration text).

  9. def OAI.BoundedRecovery.StandardModularData.ScalarCentralizer line 69

    Also declared: ComparatorChallenges/BoundedRecovery.lean:69 (same declaration text).

  10. def OAI.BoundedRecovery.symmetricAverage line 75

    Also declared: ComparatorChallenges/BoundedRecovery.lean:75 (same declaration text).

  11. def OAI.BoundedRecovery.fixedMean line 78

    Also declared: ComparatorChallenges/BoundedRecovery.lean:78 (same declaration text).

  12. def OAI.BoundedRecovery.RecoveryConclusion line 81

    Also declared: ComparatorChallenges/BoundedRecovery.lean:81 (same declaration text).

  13. def OAI.BoundedRecovery.StandardModularData.state line 90