OAI/NumberTheory/DirichletL/MeanSquare/UnitRows.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompletedUnitRows.unitRowFamily line 85
  2. lemma OAI.CompletedUnitRows.unitRowFamily_norm line 89
  3. lemma OAI.CompletedUnitRows.rowTwist_normHeight line 93
  4. theorem OAI.CompletedUnitRows.short_completed_elements_uniform_twist line 99
  5. structure OAI.SecondPassArithmetic.CanonicalStateCondition line 168
  6. theorem OAI.SecondPassArithmetic.CanonicalStateCondition.invariant_reserved line 181
  7. theorem OAI.SecondPassArithmetic.CanonicalStateCondition.small_or_live line 190
  8. theorem OAI.SecondPassArithmetic.canonicalStateCondition_retained line 212
  9. theorem OAI.SecondPassArithmetic.canonicalStateCondition_cutoff_retained line 267
  10. theorem OAI.SecondPassArithmetic.nonzeroRowFamily_le_center line 324
  11. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_nonzero_twoPassage line 354
  12. def OAI.CubicEisenstein.euclideanAxisPath line 427
  13. lemma OAI.CubicEisenstein.euclideanAxisPath_affine line 430
  14. lemma OAI.CubicEisenstein.euclideanAxisPath_self line 439
  15. lemma OAI.CubicEisenstein.euclideanAxisPath_hasDerivAt line 443
  16. lemma OAI.CubicEisenstein.euclideanAxisSlice_deriv line 451
  17. lemma OAI.CubicEisenstein.euclideanAxisSlice_derivatives line 457
  18. def OAI.CubicEisenstein.positiveEuclideanLaplacian line 482
  19. lemma OAI.CubicEisenstein.positiveEuclideanLaplacian_eq_axis line 486
  20. lemma OAI.CubicEisenstein.positiveEuclideanLaplacian_congr line 493
  21. lemma OAI.CubicEisenstein.kernelTestPartitionTerm_tsupport_right line 507
  22. lemma OAI.CubicEisenstein.kernelSmoothTest_finite_chart_partition_subsupport line 513
  23. lemma OAI.CubicEisenstein.kernelDirichletForm_supported_equation_chart line 529
  24. theorem OAI.CubicEisenstein.kernelDirichletForm_supported_equation line 580