OAI/Analysis/ModularRecovery/Recovery.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded recovery on exact factor-four spectral bands.

  1. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.real_smul line 17
  2. lemma OAI.BoundedRecovery.RealSpectralCalculus.HasSpectralSupport.sum line 23
  3. lemma OAI.BoundedRecovery.phaseSum_mem line 29
  4. lemma OAI.BoundedRecovery.phaseSum_vector_support line 33
  5. lemma OAI.BoundedRecovery.norm_sq_le_twice_sum line 40
  6. lemma OAI.BoundedRecovery.StandardModularData.bounded_recovery_finite_step line 47
  7. def OAI.BoundedRecovery.recoveryMomentBound line 118
  8. lemma OAI.BoundedRecovery.recoveryMomentBound_pos line 120
  9. lemma OAI.BoundedRecovery.exists_recovery_cutoff line 125
  10. lemma OAI.BoundedRecovery.StandardModularData.moment_bound_of_narrow_band line 144
  11. lemma OAI.BoundedRecovery.StandardModularData.exists_band_representative_with_defect line 176
  12. lemma OAI.BoundedRecovery.StandardModularData.bounded_recovery_single line 202
  13. theorem OAI.BoundedRecovery.bounded_recovery line 227

    Distinct definitions of this name: ComparatorChallenges/BoundedRecovery.lean:88 (same statement text; different proof or body). Qualify references as OAI.BoundedRecovery.bounded_recovery@path.