OAI/NumberTheory/DirichletL/Eisenstein/FredholmAlternative.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.ker_orthogonal_restriction_injective line 87
  2. lemma OAI.CubicEisenstein.ker_orthogonal_restriction_range line 96
  3. lemma OAI.CubicEisenstein.ker_orthogonal_restriction_antilipschitz line 109
  4. lemma OAI.CubicEisenstein.closed_range_of_compact_estimate line 118
  5. lemma OAI.CubicEisenstein.selfAdjoint_range_eq_ker_orthogonal line 126
  6. lemma OAI.CubicEisenstein.selfAdjoint_fredholm_of_compact_estimate line 139
  7. def OAI.CubicEisenstein.kernelSpectralFormOperator line 162
  8. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_inner line 166
  9. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_selfAdjoint line 175
  10. lemma OAI.CubicEisenstein.scalar_compact_energy_estimate line 189
  11. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_compact_estimate line 207
  12. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_solution_graph line 222
  13. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_of_domain line 237
  14. theorem OAI.CubicEisenstein.kernelSpectralFormOperator_isFredholm line 249
  15. theorem OAI.CubicEisenstein.kernel_theta_spectral_fredholm line 259
  16. theorem OAI.CanonicalRowCompletion.cubeLogRange_sq_small_power line 269
  17. theorem OAI.SecondPassArithmetic.halfCanonicalPadding_budget line 320
  18. theorem OAI.SecondPassArithmetic.canonicalRankMargin_strict_reserve line 330
  19. theorem OAI.SecondPassArithmetic.CanonicalStateCondition.fixed_factor_margin line 336
  20. theorem OAI.CanonicalRowCompletion.height_sum_bound line 372
  21. theorem OAI.CanonicalRowCompletion.progressingCanonicalBin_energy line 379
  22. theorem OAI.CompletedGauss.shortCompletedSum_nonpos line 456
  23. theorem OAI.CanonicalRowCompletion.canonicalLabels_subset_idealRange line 472
  24. theorem OAI.CanonicalRowCompletion.rowFamilyEnergy_le_rectangle line 481
  25. theorem OAI.CanonicalRowCompletion.canonicalShortEnergy_uniform_twist line 508
  26. theorem OAI.CanonicalRowCompletion.progressingCanonicalFamily_energy line 558