OAI/Analysis/Triangular/Basic.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.AtomicTriangular.Plane line 11

   Also declared: ComparatorChallenges/AtomicGaussian.lean:11 (same declaration text), ComparatorChallenges/TriangularEnergy.lean:42 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:18 (same declaration text).

2. def OAI.AtomicTriangular.b line 13

   Also declared: ComparatorChallenges/AtomicGaussian.lean:13 (same declaration text), ComparatorChallenges/TriangularEnergy.lean:44 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:20 (same declaration text).

3. def OAI.AtomicTriangular.triangularPoint line 15

   Also declared: ComparatorChallenges/AtomicGaussian.lean:15 (same declaration text), ComparatorChallenges/TriangularEnergy.lean:46 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:22 (same declaration text).

4. def OAI.AtomicTriangular.A line 20

   Also declared: ComparatorChallenges/AtomicGaussian.lean:20 (same declaration text), ComparatorChallenges/TriangularEnergy.lean:51 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:27 (same declaration text).

5. def OAI.AtomicTriangular.dualA line 22

   Also declared: ComparatorChallenges/AtomicGaussian.lean:22 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:29 (same declaration text).

6. def OAI.AtomicTriangular.gaussian line 24

   Also declared: ComparatorChallenges/AtomicGaussian.lean:24 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:31 (same declaration text).

7. def OAI.AtomicTriangular.Radial line 26

   Also declared: ComparatorChallenges/AtomicGaussian.lean:26 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:33 (same declaration text).

8. def OAI.AtomicTriangular.realFourier line 28

   Also declared: ComparatorChallenges/AtomicGaussian.lean:28 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:35 (same declaration text).

9. def OAI.AtomicTriangular.Construction.b line 34

   Also declared: ComparatorChallenges/AtomicGaussian.lean:34 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:41 (same declaration text).

10. def OAI.AtomicTriangular.Construction.h line 36

    Also declared: ComparatorChallenges/AtomicGaussian.lean:36 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:43 (same declaration text).

11. def OAI.AtomicTriangular.Construction.H line 38

    Also declared: ComparatorChallenges/AtomicGaussian.lean:38 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:45 (same declaration text).

12. def OAI.AtomicTriangular.Construction.eta line 40

    Also declared: ComparatorChallenges/AtomicGaussian.lean:40 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:47 (same declaration text).

13. def OAI.AtomicTriangular.Construction.kappa line 42

    Also declared: ComparatorChallenges/AtomicGaussian.lean:42 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:49 (same declaration text).

14. def OAI.AtomicTriangular.Construction.residues line 44

    Also declared: ComparatorChallenges/AtomicGaussian.lean:44 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:51 (same declaration text).

15. def OAI.AtomicTriangular.Construction.residue line 46

    Also declared: ComparatorChallenges/AtomicGaussian.lean:46 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:53 (same declaration text).

16. def OAI.AtomicTriangular.Construction.Node line 48

    Also declared: ComparatorChallenges/AtomicGaussian.lean:48 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:55 (same declaration text).

17. def OAI.AtomicTriangular.Construction.FiniteNodes line 50

    Also declared: ComparatorChallenges/AtomicGaussian.lean:50 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:57 (same declaration text).

18. def OAI.AtomicTriangular.Construction.sineFactor line 52

    Also declared: ComparatorChallenges/AtomicGaussian.lean:52 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:59 (same declaration text).

19. def OAI.AtomicTriangular.Construction.P line 55

    Also declared: ComparatorChallenges/AtomicGaussian.lean:55 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:62 (same declaration text).

20. def OAI.AtomicTriangular.Construction.dBasis line 57

    Also declared: ComparatorChallenges/AtomicGaussian.lean:57 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:64 (same declaration text).

21. def OAI.AtomicTriangular.Construction.cBasis line 59

    Also declared: ComparatorChallenges/AtomicGaussian.lean:59 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:66 (same declaration text).

22. def OAI.AtomicTriangular.Construction.finiteC line 61

    Also declared: ComparatorChallenges/AtomicGaussian.lean:61 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:68 (same declaration text).

23. def OAI.AtomicTriangular.Construction.finiteD line 64

    Also declared: ComparatorChallenges/AtomicGaussian.lean:64 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:71 (same declaration text).

24. def OAI.AtomicTriangular.Construction.phase line 69

    Also declared: ComparatorChallenges/AtomicGaussian.lean:69 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:76 (same declaration text).

25. def OAI.AtomicTriangular.Construction.atomFactor line 71

    Also declared: ComparatorChallenges/AtomicGaussian.lean:71 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:78 (same declaration text).

26. def OAI.AtomicTriangular.Construction.atomPolynomial line 74

    Also declared: ComparatorChallenges/AtomicGaussian.lean:74 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:81 (same declaration text).

27. def OAI.AtomicTriangular.Construction.cAtomPolynomial line 76

    Also declared: ComparatorChallenges/AtomicGaussian.lean:76 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:83 (same declaration text).

28. def OAI.AtomicTriangular.Construction.dAtomPolynomial line 79

    Also declared: ComparatorChallenges/AtomicGaussian.lean:79 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:86 (same declaration text).

29. def OAI.AtomicTriangular.Construction.fourierCoeff line 84

    Also declared: ComparatorChallenges/AtomicGaussian.lean:84 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:91 (same declaration text).

30. def OAI.AtomicTriangular.Construction.frequency line 86

    Also declared: ComparatorChallenges/AtomicGaussian.lean:86 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:93 (same declaration text).

31. def OAI.AtomicTriangular.Construction.waveDerivative line 88

    Also declared: ComparatorChallenges/AtomicGaussian.lean:88 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:95 (same declaration text).

32. def OAI.AtomicTriangular.Construction.Q line 92

    Also declared: ComparatorChallenges/AtomicGaussian.lean:92 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:99 (same declaration text).

33. def OAI.AtomicTriangular.Construction.D line 94

    Also declared: ComparatorChallenges/AtomicGaussian.lean:94 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:101 (same declaration text).

34. def OAI.AtomicTriangular.FiniteCertificate.cShiftPolynomial line 101

    Also declared: ComparatorChallenges/AtomicGaussian.lean:101 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:108 (same declaration text).

35. def OAI.AtomicTriangular.FiniteCertificate.cCoefficient line 103

    Also declared: ComparatorChallenges/AtomicGaussian.lean:103 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:110 (same declaration text).

36. def OAI.AtomicTriangular.FiniteCertificate.dCoefficient line 105

    Also declared: ComparatorChallenges/AtomicGaussian.lean:105 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:112 (same declaration text).

37. abbrev OAI.AtomicTriangular.Construction.Plane line 111

    Also declared: ComparatorChallenges/AtomicGaussian.lean:111 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:118 (same declaration text).

38. def OAI.AtomicTriangular.Construction.radial line 113

    Also declared: ComparatorChallenges/AtomicGaussian.lean:113 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:120 (same declaration text).

39. def OAI.AtomicTriangular.Construction.waveDen line 115

    Also declared: ComparatorChallenges/AtomicGaussian.lean:115 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:122 (same declaration text).

40. def OAI.AtomicTriangular.Construction.Xwave line 117

    Also declared: ComparatorChallenges/AtomicGaussian.lean:117 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:124 (same declaration text).

41. def OAI.AtomicTriangular.Construction.lambda line 119

    Also declared: ComparatorChallenges/AtomicGaussian.lean:119 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:126 (same declaration text).

42. def OAI.AtomicTriangular.Construction.zeta line 121

    Also declared: ComparatorChallenges/AtomicGaussian.lean:121 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:128 (same declaration text).

43. def OAI.AtomicTriangular.Construction.transformedWave line 123

    Also declared: ComparatorChallenges/AtomicGaussian.lean:123 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:130 (same declaration text).

44. def OAI.AtomicTriangular.Construction.finiteColumn line 125

    Also declared: ComparatorChallenges/AtomicGaussian.lean:125 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:132 (same declaration text).

45. def OAI.AtomicTriangular.Construction.finiteNode line 131

    Also declared: ComparatorChallenges/AtomicGaussian.lean:131 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:138 (same declaration text).

46. def OAI.AtomicTriangular.Construction.jetMultiplier line 133

    Also declared: ComparatorChallenges/AtomicGaussian.lean:133 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:140 (same declaration text).

47. def OAI.AtomicTriangular.Construction.jet line 137

    Also declared: ComparatorChallenges/AtomicGaussian.lean:137 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:144 (same declaration text).

48. def OAI.AtomicTriangular.Construction.fullJetMatrix line 140

    Also declared: ComparatorChallenges/AtomicGaussian.lean:140 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:147 (same declaration text).

49. def OAI.AtomicTriangular.Construction.R line 144

    Also declared: ComparatorChallenges/AtomicGaussian.lean:144 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:151 (same declaration text).

50. def OAI.AtomicTriangular.Construction.R0 line 146

    Also declared: ComparatorChallenges/AtomicGaussian.lean:146 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:153 (same declaration text).

51. abbrev OAI.AtomicTriangular.Construction.TailNode line 149

    Also declared: ComparatorChallenges/AtomicGaussian.lean:149 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:156 (same declaration text).

52. structure OAI.AtomicTriangular.Construction.InputCoefficients line 151

    Also declared: ComparatorChallenges/AtomicGaussian.lean:151 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:158 (same declaration text).

53. def OAI.AtomicTriangular.Construction.tailInput line 159

    Also declared: ComparatorChallenges/AtomicGaussian.lean:159 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:166 (same declaration text).

54. def OAI.AtomicTriangular.Construction.finiteInput line 162

    Also declared: ComparatorChallenges/AtomicGaussian.lean:162 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:169 (same declaration text).

55. def OAI.AtomicTriangular.Construction.inputComplex line 166

    Also declared: ComparatorChallenges/AtomicGaussian.lean:166 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:173 (same declaration text).

56. def OAI.AtomicTriangular.Construction.Z line 170

    Also declared: ComparatorChallenges/AtomicGaussian.lean:170 (same declaration text).

57. def OAI.AtomicTriangular.Construction.targetCoefficient line 172

    Also declared: ComparatorChallenges/AtomicGaussian.lean:172 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:177 (same declaration text).

58. def OAI.AtomicTriangular.Construction.Yf line 174

    Also declared: ComparatorChallenges/AtomicGaussian.lean:174 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:179 (same declaration text).

59. def OAI.AtomicTriangular.Construction.gamma line 181

    Also declared: ComparatorChallenges/AtomicGaussian.lean:181 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:186 (same declaration text).

60. def OAI.AtomicTriangular.Construction.Uplus line 184

    Also declared: ComparatorChallenges/AtomicGaussian.lean:184 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:189 (same declaration text).

61. def OAI.AtomicTriangular.Construction.Uminus line 187

    Also declared: ComparatorChallenges/AtomicGaussian.lean:187 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:192 (same declaration text).

62. def OAI.AtomicTriangular.Construction.finiteSolution line 190

    Also declared: ComparatorChallenges/AtomicGaussian.lean:190 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:195 (same declaration text).

63. def OAI.AtomicTriangular.Construction.Acoefficient line 193

    Also declared: ComparatorChallenges/AtomicGaussian.lean:193 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:198 (same declaration text).

64. def OAI.AtomicTriangular.Construction.gaussianZ line 198

    Also declared: ComparatorChallenges/AtomicGaussian.lean:198 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:203 (same declaration text).

65. def OAI.AtomicTriangular.Construction.actualParameter line 200

    Also declared: ComparatorChallenges/AtomicGaussian.lean:200 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:205 (same declaration text).

66. def OAI.AtomicTriangular.Construction.normalizingDen line 204

    Also declared: ComparatorChallenges/AtomicGaussian.lean:204 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:209 (same declaration text).

67. def OAI.AtomicTriangular.Construction.finiteCoordinates line 210

    Also declared: ComparatorChallenges/AtomicGaussian.lean:210 (same declaration text).

68. def OAI.AtomicTriangular.Construction.HasAtomicConstruction line 214

    Also declared: ComparatorChallenges/AtomicGaussian.lean:214 (same declaration text).