OAI/NumberTheory/DirichletL/MeanSquare/SourceTransfer.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InitialMeanSquare.residualScale line 89
  2. def OAI.InitialMeanSquare.sourceWeight line 93
  3. theorem OAI.InitialMeanSquare.sourceWeight_norm_le line 98
  4. theorem OAI.InitialMeanSquare.initial_source_fixed_profiles line 112
  5. def OAI.InitialMeanSquare.sourceElementData line 195
  6. def OAI.InitialMeanSquare.sourceObservation line 200
  7. lemma OAI.InitialMeanSquare.sourceObservation_eq line 205
  8. theorem OAI.InitialMeanSquare.sourceElementData_injective line 210
  9. theorem OAI.InitialMeanSquare.source_fiber_card_le line 226
  10. theorem OAI.InitialMeanSquare.source_weighted_energy_pushforward line 243
  11. theorem OAI.InitialMeanSquare.source_weighted_cauchy line 272
  12. abbrev OAI.CubicEisenstein.EuclideanL2 line 308
  13. abbrev OAI.CubicEisenstein.EuclideanGradientL2 line 309
  14. example OAI.CubicEisenstein.(example at line 310) line 310
  15. example OAI.CubicEisenstein.(example at line 311) line 311
  16. abbrev OAI.CubicEisenstein.EuclideanDistributions line 312
  17. def OAI.CubicEisenstein.euclideanCoordinateVector line 314
  18. def OAI.CubicEisenstein.euclideanL2Distribution line 315
  19. lemma OAI.CubicEisenstein.euclideanL2Distribution_injective line 318
  20. def OAI.CubicEisenstein.euclideanGradientEquations line 322
  21. def OAI.CubicEisenstein.euclideanWeakGradientGraph line 330
  22. lemma OAI.CubicEisenstein.mem_euclideanWeakGradientGraph line 333
  23. lemma OAI.CubicEisenstein.euclideanWeakGradientGraph_unique line 340
  24. def OAI.CubicEisenstein.euclideanWeakGradient line 349
  25. lemma OAI.CubicEisenstein.euclideanWeakGradient_graph line 352
  26. theorem OAI.CubicEisenstein.euclideanWeakGradient_closed line 355
  27. lemma OAI.CubicEisenstein.schwartz_mem_euclideanWeakGradientGraph line 359
  28. theorem OAI.CubicEisenstein.euclideanWeakGradient_dense_domain line 367
  29. abbrev OAI.CubicEisenstein.EuclideanH1Ambient line 380
  30. def OAI.CubicEisenstein.euclideanH1Submodule line 382
  31. lemma OAI.CubicEisenstein.euclideanH1Submodule_isClosed line 385
  32. abbrev OAI.CubicEisenstein.EuclideanH1 line 390
  33. instance OAI.CubicEisenstein.euclideanH1Complete line 392
  34. example OAI.CubicEisenstein.(example at line 394) line 394
  35. def OAI.CubicEisenstein.euclideanH1Embedding line 396
  36. def OAI.CubicEisenstein.euclideanH1Gradient line 401
  37. lemma OAI.CubicEisenstein.euclideanH1Embedding_eq_zero line 406
  38. lemma OAI.CubicEisenstein.euclideanH1Embedding_injective line 413
  39. lemma OAI.CubicEisenstein.euclideanH1Embedding_dense line 419
  40. lemma OAI.CubicEisenstein.euclideanH1_norm_sq line 427
  41. def OAI.InitialMeanSquare.normCharacter line 438
  42. lemma OAI.InitialMeanSquare.normCharacter_prod line 445
  43. lemma OAI.InitialMeanSquare.pool_support_product line 451
  44. theorem OAI.InitialMeanSquare.sum_selected_ideals line 461
  45. def OAI.InitialMeanSquare.selectedIdealTest line 480
  46. theorem OAI.InitialMeanSquare.idealRowSum_eq_mobiusRow line 483
  47. def OAI.InitialMeanSquare.sourceChildEnergy line 528
  48. def OAI.InitialMeanSquare.sourceEnergyMagnitude line 533
  49. lemma OAI.InitialMeanSquare.sourceChildEnergy_le line 538
  50. lemma OAI.InitialMeanSquare.sourceChildEnergy_continuous line 547
  51. def OAI.InitialMeanSquare.sourceGeometricMean line 556
  52. def OAI.InitialMeanSquare.sourceFixedMode line 561
  53. def OAI.InitialMeanSquare.integratedSourceMode line 569
  54. theorem OAI.InitialMeanSquare.weighted_conjugate_pair_swap line 577
  55. theorem OAI.InitialMeanSquare.integrated_source_transfer line 589