OAI/NumberTheory/Catalan/Estimates/RealEnergySupDual.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.energy_damping_log_cost line 18
  2. theorem OAI.InternalCatalan.realEnergy_cosine_tau_le line 32
  3. theorem OAI.InternalCatalan.realEnergy_cosine_sigma_le line 44
  4. theorem OAI.InternalCatalan.trial_scalar_norm_le line 64
  5. theorem OAI.InternalCatalan.trial_abs_tail_le line 77
  6. theorem OAI.InternalCatalan.barrierTrialT_abs_le line 84
  7. theorem OAI.InternalCatalan.barrierTrialS_abs_le line 97
  8. theorem OAI.InternalCatalan.energy_sum_pairs_of_symmetric line 117
  9. theorem OAI.InternalCatalan.energy_sum_pairs_one line 145
  10. theorem OAI.InternalCatalan.energy_sum_pairs_const line 158
  11. theorem OAI.InternalCatalan.energy_sum_pairs_le_of_le_add line 165
  12. theorem OAI.InternalCatalan.realEnergyCosineKernel_symm line 181
  13. def OAI.InternalCatalan.realEnergyField line 202
  14. def OAI.InternalCatalan.realEnergyColumnField line 206
  15. def OAI.InternalCatalan.realEnergyCaseField line 209
  16. def OAI.InternalCatalan.realEnergyFiniteValue line 212
  17. theorem OAI.InternalCatalan.realEnergyMajorantOne_finite line 224
  18. theorem OAI.InternalCatalan.realEnergyMajorantTwo_finite line 240
  19. theorem OAI.InternalCatalan.realEnergyCaseField_eq line 262
  20. theorem OAI.InternalCatalan.realEnergyCaseField_average line 269
  21. theorem OAI.InternalCatalan.realEnergyCaseField_average_gt line 278
  22. theorem OAI.InternalCatalan.realEnergyCaseField_correction line 299
  23. def OAI.InternalCatalan.realEnergyOffDiagonalInteraction line 316
  24. theorem OAI.InternalCatalan.realEnergyOffDiagonalInteraction_le_damped line 323
  25. def OAI.InternalCatalan.realEnergyRegularizationError line 417
  26. theorem OAI.InternalCatalan.realEnergyFiniteValue_le_regularized line 424
  27. def OAI.InternalCatalan.realEnergyRowTrialField line 483
  28. def OAI.InternalCatalan.realEnergyColumnTrialField line 487
  29. theorem OAI.InternalCatalan.realEnergyFiniteValue_le_trialFields line 490
  30. theorem OAI.InternalCatalan.realEnergyRowTrialField_residual_le line 540
  31. theorem OAI.InternalCatalan.realEnergyColumnTrialField_residual_le line 560
  32. theorem OAI.InternalCatalan.energy_endpoint_convex_bound line 570
  33. theorem OAI.InternalCatalan.realEnergyRowTrialField_weaken_le line 577
  34. theorem OAI.InternalCatalan.realEnergyColumnTrialField_weaken_le line 595
  35. def OAI.InternalCatalan.realEnergyDualConstant line 612
  36. def OAI.InternalCatalan.realEnergyDualDampingCoefficient line 615
  37. def OAI.InternalCatalan.realEnergyDualFiniteCoefficient line 618
  38. theorem OAI.InternalCatalan.realEnergyRegularizationError_le line 624
  39. theorem OAI.InternalCatalan.realEnergyFiniteValue_le_uniformDual line 644
  40. theorem OAI.InternalCatalan.realEnergyDualDampingCoefficient_nonneg line 689
  41. theorem OAI.InternalCatalan.realEnergy_uniform_dual_eventually line 696
  42. theorem OAI.InternalCatalan.realEnergyMajorantOne_uniform_dual line 745
  43. theorem OAI.InternalCatalan.realEnergyMajorantTwo_uniform_dual line 765
  44. def OAI.InternalCatalan.realEnergyRowTrialSup line 787
  45. def OAI.InternalCatalan.realEnergyColumnTrialSup line 790
  46. theorem OAI.InternalCatalan.realEnergyRowTrialField_image_bddAbove line 793
  47. theorem OAI.InternalCatalan.realEnergyColumnTrialField_image_bddAbove line 805
  48. theorem OAI.InternalCatalan.realEnergyRowTrialField_image_nonempty line 815
  49. theorem OAI.InternalCatalan.realEnergyColumnTrialField_image_nonempty line 820
  50. theorem OAI.InternalCatalan.realEnergyRowTrialField_le_sup line 825
  51. theorem OAI.InternalCatalan.realEnergyColumnTrialField_le_sup line 832
  52. theorem OAI.InternalCatalan.realEnergy_uniform_sup_dual_eventually line 837