OAI/MathematicalPhysics/Elasticity/BoundarySymbols.lean

GitHub source file

152 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElasticityBoundaryProfile.Y line 13

   Source comment

   All coordinate spaces here carry the standard finite-product Euclidean topology.

   abbrev Y := Fin 3 → ℝ

2. def OAI.ElasticityBoundaryProfile.phase line 15
3. def OAI.ElasticityBoundaryProfile.envelope line 16
4. def OAI.ElasticityBoundaryProfile.profile line 17
5. def OAI.ElasticityBoundaryProfile.conjugateDerivative line 19
6. lemma OAI.ElasticityBoundaryProfile.conjugateDerivative_apply line 22
7. lemma OAI.ElasticityBoundaryProfile.smooth_profile line 25
8. theorem OAI.ElasticityBoundaryProfile.fderiv_profile_basis line 30

   Source documentation

   Each formal conjugated partial is exactly the Frechet derivative of the actual function in a coordinate direction.

   theorem fderiv_profile_basis (δ : ℝ) (p : MP) (y : Y) (j : Fin 3) :
       fderiv ℝ (profile δ p) y (Pi.single j 1)=profile δ (conjugateDerivative δ j p) y := by
   …

   Mentions: OAI.ElasticityBoundaryProfile.Y, OAI.ElasticityBoundaryProfile.profile, OAI.ElasticityBoundaryProfile.conjugateDerivative

9. def OAI.ElasticityBoundaryProfile.D line 41

   Source documentation

   Polynomial dependence on the concentration parameter after multiplying the physical derivative by delta squared.

   def D (δ : ℝ) (j : Fin 3) : MP →ₗ[ℂ] MP :=
   …

10. lemma OAI.ElasticityBoundaryProfile.phase_partial line 47
11. lemma OAI.ElasticityBoundaryProfile.conjugate_zero line 52
12. lemma OAI.ElasticityBoundaryProfile.conjugate_one line 58
13. lemma OAI.ElasticityBoundaryProfile.conjugate_two line 63
14. lemma OAI.ElasticityBoundaryProfile.D_eq_scaled line 67
15. lemma OAI.ElasticityBoundaryProfile.scale_basis line 78
16. def OAI.ElasticityBoundaryProfile.physicalProfile line 85
17. lemma OAI.ElasticityBoundaryProfile.smooth_physicalProfile line 87
18. theorem OAI.ElasticityBoundaryProfile.fderiv_physicalProfile_basis line 92

    Source documentation

    The true derivative in unscaled boundary coordinates.

    theorem fderiv_physicalProfile_basis {δ : ℝ} (hδ : δ≠0) (p : MP) (z : Y) (j : Fin 3) :
        fderiv ℝ (physicalProfile δ p) z (Pi.single j 1) =
          ((δ^2)⁻¹:ℝ) • physicalProfile δ (D δ j p) z := by
    …

    Mentions: OAI.ElasticityBoundaryProfile.Y, OAI.ElasticityBoundaryProfile.physicalProfile, OAI.ElasticityBoundaryProfile.D

19. lemma OAI.ElasticityBoundaryProfile.phase_real line 105
20. lemma OAI.ElasticityBoundaryProfile.envelope_norm line 109
21. theorem OAI.ElasticityBoundaryProfile.profile_square_weight line 115

    Source documentation

    Modulus squared is the proved integrable Gaussian/normal weight; the fast oscillation does not alter it at any nonzero scale.

    theorem profile_square_weight (δ : ℝ) (p : MP) (y : Y) :
        ({y : Y | 0<y 2} : Set Y).indicator (fun y => ‖profile δ p y‖^2) y =
          ‖value p y‖^2 * weight 2 y := by
    …

    Mentions: OAI.ElasticityBoundaryProfile.Y, OAI.ElasticityBoundaryProfile.profile

22. def OAI.ElasticityBoundaryParameter.coeffMap line 142
23. lemma OAI.ElasticityBoundaryParameter.coeffMap_monomial line 147
24. lemma OAI.ElasticityBoundaryParameter.coeffMap_coeff line 151
25. lemma OAI.ElasticityBoundaryParameter.coeffMap_C line 160
26. lemma OAI.ElasticityBoundaryParameter.coeffMap_X_mul line 164
27. lemma OAI.ElasticityBoundaryParameter.coeffMap_monomial_one_mul line 170
28. lemma OAI.ElasticityBoundaryParameter.eval_coeffMap line 178
29. def OAI.ElasticityBoundaryParameter.E₀ line 188

    Source documentation

    The parameter-independent and linear parts of the actual scaled derivative.

    def E₀ (j : Fin 3) : MP →ₗ[ℂ] MP :=
    …

30. def OAI.ElasticityBoundaryParameter.E₁ line 192
31. lemma OAI.ElasticityBoundaryParameter.D_expansion line 196
32. def OAI.ElasticityBoundaryParameter.PD line 199
33. lemma OAI.ElasticityBoundaryParameter.PD_apply line 202
34. lemma OAI.ElasticityBoundaryParameter.eval_PD line 205
35. lemma OAI.ElasticityBoundaryParameter.PD_monomial_one_mul line 214
36. abbrev OAI.ElasticityBoundarySymbol.F line 232
37. def OAI.ElasticityBoundarySymbol.slope line 234
38. def OAI.ElasticityBoundarySymbol.solution line 238
39. def OAI.ElasticityBoundarySymbol.first line 241
40. def OAI.ElasticityBoundarySymbol.second line 244
41. lemma OAI.ElasticityBoundarySymbol.solution_derivative line 247
42. lemma OAI.ElasticityBoundarySymbol.first_derivative line 255
43. lemma OAI.ElasticityBoundarySymbol.solution_boundary line 264
44. def OAI.ElasticityBoundarySymbol.fourierDiv line 268
45. def OAI.ElasticityBoundarySymbol.fourierGradDiv line 271
46. def OAI.ElasticityBoundarySymbol.fourierPhysical line 275
47. theorem OAI.ElasticityBoundarySymbol.solution_physical line 280

    Source documentation

    Literal Fourier-transformed constant elasticity PDE, not a prescribed symbol assigned by definition to the DN map.

    theorem solution_physical (l m : ℂ) (hp : l+3*m≠0) (f : F) (t : ℝ) :
        fourierPhysical l m f t=0 := by
    …

    Mentions: OAI.ElasticityBoundarySymbol.F, OAI.ElasticityBoundarySymbol.fourierPhysical

48. def OAI.ElasticityBoundarySymbol.traction line 292
49. def OAI.ElasticityBoundarySymbol.symbol line 296
50. theorem OAI.ElasticityBoundarySymbol.traction_symbol line 301
51. theorem OAI.ElasticityBoundarySymbol.symbol_injective line 314

    Source documentation

    Both constants are encoded in the principal symbol.

    theorem symbol_injective {l₁ m₁ l₂ m₂ : ℂ} (hm : m₁≠0)
        (hp₁ : l₁+3*m₁≠0) (hp₂ : l₂+3*m₂≠0)
        (hs : symbol l₁ m₁=symbol l₂ m₂) : l₁=l₂ ∧ m₁=m₂ := by
    …

    Mentions: OAI.ElasticityBoundarySymbol.symbol

52. theorem OAI.ElasticityBoundarySymbol.real_symbol_injective line 328
53. abbrev OAI.ElasticityBoundarySymbol.P line 352
54. def OAI.ElasticityBoundarySymbol.shiftedDerivative line 355

    Source documentation

    Differentiation of the polynomial amplitude after factoring out exp(-t).

    def shiftedDerivative (c : ℂ) : P →ₗ[ℂ] P :=
    …

    Mentions: OAI.ElasticityBoundarySymbol.P

55. lemma OAI.ElasticityBoundarySymbol.shiftedDerivative_apply line 358
56. lemma OAI.ElasticityBoundarySymbol.polynomial_derivative_surjective line 361
57. lemma OAI.ElasticityBoundarySymbol.shiftedDerivative_surjective line 375

    Source documentation

    Although differentiation is nilpotent only degree by degree, each nonzero scalar shift is onto the whole space of finite polynomials.

    lemma shiftedDerivative_surjective (c : ℂ) (hc : c≠0) :
        Function.Surjective (shiftedDerivative c) := by
    …

    Mentions: OAI.ElasticityBoundarySymbol.shiftedDerivative

58. def OAI.ElasticityBoundarySymbol.laplaceAmplitude line 405

    Source documentation

    The amplitude operator for d²/dt²-1 on exp(-t) times a polynomial.

    def laplaceAmplitude : P →ₗ[ℂ] P :=
    …

    Mentions: OAI.ElasticityBoundarySymbol.P

59. lemma OAI.ElasticityBoundarySymbol.laplaceAmplitude_apply line 408
60. lemma OAI.ElasticityBoundarySymbol.laplaceAmplitude_surjective line 412
61. lemma OAI.ElasticityBoundarySymbol.laplaceAmplitude_commutes line 415
62. lemma OAI.ElasticityBoundarySymbol.shiftedDerivative_sq line 421
63. def OAI.ElasticityBoundarySymbol.polynomialPhysical line 428

    Source documentation

    The actual Fourier-transformed isotropic physical elasticity operator on polynomial amplitudes, tangential covector (1,0), inward normal t.

    def polynomialPhysical (l m : ℂ) (p : Fin 3 → P) : Fin 3 → P :=
    …

    Mentions: OAI.ElasticityBoundarySymbol.P

64. def OAI.ElasticityBoundarySymbol.polynomialAdjugate line 437

    Source documentation

    A polynomial differential adjugate; the middle polarization uses the same scalar determinant, so all three components admit one uniform construction.

    def polynomialAdjugate (l m : ℂ) (p : Fin 3 → P) : Fin 3 → P :=
    …

    Mentions: OAI.ElasticityBoundarySymbol.P

65. lemma OAI.ElasticityBoundarySymbol.polynomial_adjugate_identity line 444
66. theorem OAI.ElasticityBoundarySymbol.polynomialPhysical_surjective line 456

    Source documentation

    No exceptional polynomial degree occurs in the normal recurrence.

    theorem polynomialPhysical_surjective (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) :
        Function.Surjective (polynomialPhysical l m) := by
    …

    Mentions: OAI.ElasticityBoundarySymbol.polynomialPhysical

67. def OAI.ElasticityBoundarySymbol.homogeneousPolynomial line 481
68. lemma OAI.ElasticityBoundarySymbol.homogeneousPolynomial_boundary line 484
69. lemma OAI.ElasticityBoundarySymbol.homogeneousPolynomial_physical line 488
70. lemma OAI.ElasticityBoundarySymbol.polynomialPhysical_sub line 504
71. theorem OAI.ElasticityBoundarySymbol.polynomialPhysical_zero_boundary_surjective line 511

    Source documentation

    Every polynomial forcing has a decaying-polynomial solution with exactly zero Dirichlet data. No exceptional normal order is excluded.

    theorem polynomialPhysical_zero_boundary_surjective (l m : ℂ)
        (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0) (p : Fin 3 → P) :
        ∃ q : Fin 3 → P, polynomialPhysical l m q = p ∧ ∀ i, (q i).eval 0 = 0 := by
    …

    Mentions: OAI.ElasticityBoundarySymbol.P, OAI.ElasticityBoundarySymbol.polynomialPhysical

72. def OAI.ElasticityBoundarySymbol.decayingPolynomial line 521
73. lemma OAI.ElasticityBoundarySymbol.decayingPolynomial_derivative line 524
74. lemma OAI.ElasticityBoundarySymbol.decayingPolynomial_laplace line 534
75. def OAI.ElasticityBoundarySymbol.decayingPhysical line 542

    Source documentation

    Physical Fourier ODE, retaining the normal derivatives instead of assigning a boundary symbol by definition.

    def decayingPhysical (l m : ℂ) (q : Fin 3 → P) (t : ℝ) : F :=
    …

    Mentions: OAI.ElasticityBoundarySymbol.P, OAI.ElasticityBoundarySymbol.F

76. lemma OAI.ElasticityBoundarySymbol.decayingPhysical_eq line 552
77. theorem OAI.ElasticityBoundarySymbol.decayingPhysical_zero_boundary_surjective line 561

    Source documentation

    Literal ODE solution for each exp(-t)-polynomial forcing, with zero boundary. Its first and second derivatives are certified above.

    theorem decayingPhysical_zero_boundary_surjective (l m : ℂ)
        (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0) (p : Fin 3 → P) :
        ∃ q : Fin 3 → P,
          (∀ t, decayingPhysical l m q t = fun i => decayingPolynomial (p i) t) ∧
          ∀ i, decayingPolynomial (q i) 0 = 0 := by
    …

    Mentions: OAI.ElasticityBoundarySymbol.P, OAI.ElasticityBoundarySymbol.decayingPhysical, OAI.ElasticityBoundarySymbol.decayingPolynomial

78. abbrev OAI.ElasticityBoundaryRecursion.V line 583
79. abbrev OAI.ElasticityBoundaryRecursion.TangentialIndex line 584
80. abbrev OAI.ElasticityBoundaryRecursion.Amplitude line 585
81. def OAI.ElasticityBoundaryRecursion.normalOperator line 587
82. lemma OAI.ElasticityBoundaryRecursion.normalOperator_apply line 595
83. def OAI.ElasticityBoundaryRecursion.boundary line 600
84. lemma OAI.ElasticityBoundaryRecursion.boundary_apply line 605
85. def OAI.ElasticityBoundaryRecursion.zeroBoundary line 607
86. def OAI.ElasticityBoundaryRecursion.zeroNormalOperator line 609
87. lemma OAI.ElasticityBoundaryRecursion.zeroNormalOperator_surjective line 612
88. theorem OAI.ElasticityBoundaryRecursion.exists_normalInverse line 621

    Source documentation

    A genuine linear right inverse on the zero boundary subspace.

    theorem exists_normalInverse (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0) :
        ∃ S : V →ₗ[ℂ] V, (normalOperator l m).comp S = LinearMap.id ∧
          boundary.comp S = 0 := by
    …

    Mentions: OAI.ElasticityBoundaryRecursion.V, OAI.ElasticityBoundaryRecursion.normalOperator

89. def OAI.ElasticityBoundaryRecursion.normalAmplitude line 634

    Source documentation

    Applying the physical normal operator to each tangential monomial.

    def normalAmplitude (l m : ℂ) : Amplitude →ₗ[ℂ] Amplitude :=
    …

    Mentions: OAI.ElasticityBoundaryRecursion.Amplitude

90. def OAI.ElasticityBoundaryRecursion.boundaryAmplitude line 637
91. lemma OAI.ElasticityBoundaryRecursion.normalAmplitude_apply line 640
92. lemma OAI.ElasticityBoundaryRecursion.boundaryAmplitude_apply line 643
93. theorem OAI.ElasticityBoundaryRecursion.exists_amplitudeInverse line 646
94. theorem OAI.ElasticityBoundaryRecursion.triangular_amplitudes line 667

    Source documentation

    Successive coefficients of a triangular polynomial-amplitude equation. The zeroth coefficient is prescribed; all positive coefficients have zero physical boundary values.

    theorem triangular_amplitudes (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0)
        (A : ℕ → (Amplitude →ₗ[ℂ] Amplitude)) (hA : A 0=normalAmplitude l m)
        (p₀ : Amplitude) (h₀ : normalAmplitude l m p₀=0) :
        ∃ p : ℕ → Amplitude, p 0=p₀ ∧
          (∀ n, 0<n → boundaryAmplitude (p n)=0) ∧
          ∀ n, ∑ k ∈ Finset.range (n+1), A k (p (n-k))=0 := by
    …

    Mentions: OAI.ElasticityBoundaryRecursion.Amplitude, OAI.ElasticityBoundaryRecursion.normalAmplitude, OAI.ElasticityBoundaryRecursion.boundaryAmplitude

95. abbrev OAI.ElasticityBoundaryMVNormal.W line 715
96. def OAI.ElasticityBoundaryMVNormal.d line 717
97. def OAI.ElasticityBoundaryMVNormal.shift line 718
98. def OAI.ElasticityBoundaryMVNormal.lap line 719
99. lemma OAI.ElasticityBoundaryMVNormal.d_apply line 721
100. lemma OAI.ElasticityBoundaryMVNormal.shift_apply line 722
101. lemma OAI.ElasticityBoundaryMVNormal.lap_apply line 723
102. def OAI.ElasticityBoundaryMVNormal.normal line 726
103. lemma OAI.ElasticityBoundaryMVNormal.normal_apply line 734
104. def OAI.ElasticityBoundaryMVNormal.lift line 739
105. lemma OAI.ElasticityBoundaryMVNormal.lift_C line 741
106. lemma OAI.ElasticityBoundaryMVNormal.lift_X line 742
107. lemma OAI.ElasticityBoundaryMVNormal.d_lift line 744
108. lemma OAI.ElasticityBoundaryMVNormal.pderiv_lift line 753
109. lemma OAI.ElasticityBoundaryMVNormal.shift_lift line 755
110. lemma OAI.ElasticityBoundaryMVNormal.lap_lift line 759
111. lemma OAI.ElasticityBoundaryMVNormal.normal_lift line 763
112. lemma OAI.ElasticityBoundaryMVNormal.shift_mul line 769
113. lemma OAI.ElasticityBoundaryMVNormal.lap_mul line 771
114. lemma OAI.ElasticityBoundaryMVNormal.normal_mul line 774
115. def OAI.ElasticityBoundaryMVNormal.boundaryRing line 780

     Source documentation

     The actual restriction of a polynomial to the flat boundary.

     def boundaryRing : MP →ₐ[ℂ] MP := MvPolynomial.aeval (fun i => if i=2 then 0 else X i)

116. def OAI.ElasticityBoundaryMVNormal.boundary line 781
117. lemma OAI.ElasticityBoundaryMVNormal.boundary_apply line 782
118. lemma OAI.ElasticityBoundaryMVNormal.boundary_lift line 784
119. lemma OAI.ElasticityBoundaryMVNormal.monomial_split line 790
120. lemma OAI.ElasticityBoundaryMVNormal.normal_zeroBoundary_surjective line 795
121. theorem OAI.ElasticityBoundaryMVNormal.exists_inverse line 829

     Source documentation

     A literal multivariable-polynomial right inverse with zero boundary values.

     theorem exists_inverse (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0) :
         ∃ S : W →ₗ[ℂ] W, (normal l m).comp S=LinearMap.id ∧ boundary.comp S=0 := by
     …

     Mentions: OAI.ElasticityBoundaryMVNormal.W, OAI.ElasticityBoundaryMVNormal.normal

122. abbrev OAI.ElasticityBoundaryLayerOperator.Y line 849
123. lemma OAI.ElasticityBoundaryLayerOperator.second_physicalProfile line 851
124. def OAI.ElasticityBoundaryLayerOperator.elasticityTensor line 862

     Source documentation

     The isotropic elasticity tensor in fixed (orthonormal) coordinates.

     def elasticityTensor (l m : ℂ) (i α j β : Fin 3) : ℂ :=
     …

125. def OAI.ElasticityBoundaryLayerOperator.principal line 868

     Source documentation

     A principal tensor acts on actual polynomial conjugated derivatives.

     def principal (a : Fin 3 → Fin 3 → Fin 3 → Fin 3 → MP) (δ : ℝ) : W →ₗ[ℂ] W :=
     …

126. lemma OAI.ElasticityBoundaryLayerOperator.principal_apply line 872
127. lemma OAI.ElasticityBoundaryLayerOperator.D_zero line 876
128. theorem OAI.ElasticityBoundaryLayerOperator.principal_leading_is_normal line 882

     Source documentation

     The leading operator in the high-frequency construction is precisely the normal operator for which a zero-boundary inverse was proved.

     theorem principal_leading_is_normal (l m : ℂ) :
         principal (fun i α j β => C (elasticityTensor l m i α j β)) 0 = normal l m := by
     …

     Mentions: OAI.ElasticityBoundaryLayerOperator.principal, OAI.ElasticityBoundaryLayerOperator.elasticityTensor

129. abbrev OAI.ElasticityBoundaryTensorSeries.Tensor line 908
130. abbrev OAI.ElasticityBoundaryTensorSeries.Lower line 909
131. def OAI.ElasticityBoundaryTensorSeries.pack line 911
132. def OAI.ElasticityBoundaryTensorSeries.unpack line 914
133. lemma OAI.ElasticityBoundaryTensorSeries.pack_coeff line 916
134. lemma OAI.ElasticityBoundaryTensorSeries.unpack_pack line 921
135. lemma OAI.ElasticityBoundaryTensorSeries.pack_unpack line 926
136. lemma OAI.ElasticityBoundaryTensorSeries.eval_unpack line 930
137. lemma OAI.ElasticityBoundaryTensorSeries.eval_pack line 936
138. lemma OAI.ElasticityBoundaryTensorSeries.pack_monomial_mul line 940
139. def OAI.ElasticityBoundaryTensorSeries.operator line 945
140. lemma OAI.ElasticityBoundaryTensorSeries.unpack_operator line 952
141. theorem OAI.ElasticityBoundaryTensorSeries.eval_operator line 961

     Source documentation

     Evaluation reproduces the actual scaled principal part and the delta^2 lower-order coefficient-gradient part of a divergence-form operator.

     theorem eval_operator (a : Tensor) (b : Lower) (q : Polynomial W) (δ : ℝ) (i : Fin 3) :
         (operator a b q).eval (algebraMap ℂ W (δ:ℂ)) i =
           principal (fun i α j β => (a i α j β).eval (C (δ:ℂ))) δ
             (q.eval (algebraMap ℂ W (δ:ℂ))) i +
           (δ:ℂ)^2 • (∑ j, ∑ β, (b i j β).eval (C (δ:ℂ)) *
             D δ β ((q.eval (algebraMap ℂ W (δ:ℂ))) j)) := by
     …

     Mentions: OAI.ElasticityBoundaryTensorSeries.Tensor, OAI.ElasticityBoundaryTensorSeries.Lower, OAI.ElasticityBoundaryTensorSeries.operator

142. lemma OAI.ElasticityBoundaryTensorSeries.unpack_monomial_mul line 972
143. lemma OAI.ElasticityBoundaryTensorSeries.unpack_operator_monomial_mul line 977
144. lemma OAI.ElasticityBoundaryTensorSeries.operator_monomial_mul line 988
145. def OAI.ElasticityBoundaryTensorSeries.coefficient line 994
146. lemma OAI.ElasticityBoundaryTensorSeries.coefficient_apply line 998
147. theorem OAI.ElasticityBoundaryTensorSeries.coefficient_zero line 1003

     Source documentation

     Its leading coefficient is exactly the proved normal operator whenever its actual tensor at the base point is the isotropic physical tensor.

     theorem coefficient_zero (a : Tensor) (b : Lower) (l m : ℂ)
         (ha : ∀ i α j β, (a i α j β).coeff 0=C (elasticityTensor l m i α j β)) :
         coefficient a b 0=normal l m := by
     …

     Mentions: OAI.ElasticityBoundaryTensorSeries.Tensor, OAI.ElasticityBoundaryTensorSeries.Lower, OAI.ElasticityBoundaryTensorSeries.coefficient

148. theorem OAI.ElasticityBoundaryMVTower.triangular_amplitudes line 1032

     Source documentation

     Successive coefficients of a triangular polynomial-amplitude equation. The zeroth coefficient is prescribed; all positive coefficients have zero physical boundary values.

     theorem triangular_amplitudes (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0)
         (A : ℕ → (W →ₗ[ℂ] W)) (hA : A 0=normal l m)
         (p₀ : W) (h₀ : normal l m p₀=0) :
         ∃ p : ℕ → W, p 0=p₀ ∧
           (∀ n, 0<n → boundary (p n)=0) ∧
           ∀ n, ∑ k ∈ Finset.range (n+1), A k (p (n-k))=0 := by
     …

149. def OAI.ElasticityBoundaryMVTower.residualPolynomial line 1068

     Source documentation

     The literal residual polynomial of two finite operator/amplitude series.

     def residualPolynomial (A : ℕ → W →ₗ[ℂ] W) (p : ℕ → W) (K N : ℕ) : Polynomial W :=
     …

150. lemma OAI.ElasticityBoundaryMVTower.residual_coefficient line 1072
151. theorem OAI.ElasticityBoundaryMVTower.residual_high_order_factor line 1106

     Source documentation

     All orders up to N cancel as an exact polynomial identity, leaving an actual finite polynomial times delta^(N+1), not just a formal asymptotic.

     theorem residual_high_order_factor (A : ℕ → W →ₗ[ℂ] W) (p : ℕ → W) {K N : ℕ}
         (hKN : N≤K)
         (hc : ∀ n, ∑ k ∈ Finset.range (n+1), A k (p (n-k))=0) :
         ∃ R : Polynomial W, residualPolynomial A p K N=Polynomial.X^(N+1)*R := by
     …

     Mentions: OAI.ElasticityBoundaryMVTower.residualPolynomial

152. theorem OAI.ElasticityBoundaryMVTower.finite_physical_amplitudes line 1119

     Source documentation

     A finite correction family for every prescribed leading physical normal solution, with zero boundary corrections and exact arbitrary-order cancellation.

     theorem finite_physical_amplitudes (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0)
         (A : ℕ → W →ₗ[ℂ] W) (hA : A 0=normal l m)
         (p₀ : W) (h₀ : normal l m p₀=0) (N K : ℕ) (hKN : N≤K) :
         ∃ (p : ℕ → W) (R : Polynomial W), p 0=p₀ ∧
           (∀ n, 0<n → boundary (p n)=0) ∧
           residualPolynomial A p K N=Polynomial.X^(N+1)*R := by
     …

     Mentions: OAI.ElasticityBoundaryMVTower.residualPolynomial