OAI/Geometry/Immersion/ClosedSurface/ModeBounds.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ClosedSurfaceR4.SmallModes.ModeDomain line 19
  2. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.smoothAt line 25
  3. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.connectionX line 29
  4. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.connectionY line 34
  5. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.secondRatio line 39
  6. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_coordDeriv line 44
  7. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_connectionTerm line 49
  8. structure OAI.ClosedSurfaceR4.SmallModes.ModeCoefficientBound line 55
  9. lemma OAI.ClosedSurfaceR4.SmallModes.ModeCoefficientBound.mono_order line 65
  10. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_connectionTerm line 70
  11. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_dx line 85
  12. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_dy line 91
  13. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_mono_div_scale line 97
  14. def OAI.ClosedSurfaceR4.SmallModes.reducedConstant line 104
  15. lemma OAI.ClosedSurfaceR4.SmallModes.reducedConstant_nonneg line 107
  16. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_reducedLx line 111
  17. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_reducedLy line 136
  18. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_reducedKx line 174
  19. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_reducedKy line 183
  20. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_errorGenerator line 192
  21. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_reducedK_zero line 200
  22. def OAI.ClosedSurfaceR4.SmallModes.errorConstant line 237
  23. lemma OAI.ClosedSurfaceR4.SmallModes.errorConstant_nonneg line 240
  24. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_errorGenerator_zero line 244
  25. lemma OAI.ClosedSurfaceR4.SmallModes.errorConstant_mono line 284
  26. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_errorHierarchy line 289
  27. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_errorHierarchy_zero line 298
  28. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_tensor_complex_smul line 336
  29. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_residual_modeApprox_zero line 349
  30. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.secondForm line 378
  31. structure OAI.ClosedSurfaceR4.SmallModes.FullModeCoefficientBound line 385
  32. lemma OAI.ClosedSurfaceR4.SmallModes.FullModeCoefficientBound.mono_order line 390
  33. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_half line 394
  34. def OAI.ClosedSurfaceR4.SmallModes.targetConstant line 406
  35. lemma OAI.ClosedSurfaceR4.SmallModes.targetConstant_nonneg line 408
  36. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_reducedK line 412
  37. def OAI.ClosedSurfaceR4.SmallModes.fullErrorConstant line 457
  38. lemma OAI.ClosedSurfaceR4.SmallModes.fullErrorConstant_nonneg line 460
  39. lemma OAI.ClosedSurfaceR4.SmallModes.fullErrorConstant_mono line 465
  40. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_errorGenerator line 470
  41. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_errorHierarchy line 514
  42. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_residual_modeApprox line 552
  43. def OAI.ClosedSurfaceR4.SmallModes.tangentDualX line 585
  44. def OAI.ClosedSurfaceR4.SmallModes.tangentDualY line 588
  45. def OAI.ClosedSurfaceR4.SmallModes.normalDual line 591
  46. lemma OAI.ClosedSurfaceR4.SmallModes.tangentLift_columns line 594
  47. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.tangentDualX line 602
  48. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.tangentDualY line 609
  49. lemma OAI.ClosedSurfaceR4.SmallModes.ModeDomain.normalDual line 616
  50. structure OAI.ClosedSurfaceR4.SmallModes.ReconstructionCoefficientBound line 628
  51. lemma OAI.ClosedSurfaceR4.SmallModes.ReconstructionCoefficientBound.mono_order line 634
  52. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_smul_field line 640
  53. def OAI.ClosedSurfaceR4.SmallModes.amplitudeCorrection line 653
  54. lemma OAI.ClosedSurfaceR4.SmallModes.initialAmplitude_expansion line 659
  55. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_amplitudeCorrection line 676
  56. def OAI.ClosedSurfaceR4.SmallModes.amplitudeConstant line 685
  57. lemma OAI.ClosedSurfaceR4.SmallModes.amplitudeConstant_nonneg line 688
  58. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_amplitudeCorrection line 693
  59. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_initialAmplitude line 727
  60. def OAI.ClosedSurfaceR4.SmallModes.initialConstant line 736
  61. lemma OAI.ClosedSurfaceR4.SmallModes.initialConstant_nonneg line 738
  62. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_reconstructedLeading line 743
  63. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_scaledAmplitudeCorrection line 757
  64. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_initialAmplitude_expanded line 780
  65. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_initialAmplitude line 808
  66. lemma OAI.ClosedSurfaceR4.SmallModes.weighted_initialAmplitude_free_sub line 822
  67. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_modeApprox line 850
  68. lemma OAI.ClosedSurfaceR4.SmallModes.contDiffOn_residual line 859
  69. def OAI.ClosedSurfaceR4.SmallModes.freeModeConstant line 867
  70. lemma OAI.ClosedSurfaceR4.SmallModes.freeModeConstant_nonneg line 872
  71. theorem OAI.ClosedSurfaceR4.SmallModes.weighted_modeApprox_free_sub line 882