BoundaryLayers.lean`

129 declarations, 0 contain sorry, 0 declared as axioms

Uniform multivariable Taylor estimates for anisotropically rescaled boundary layers. The constants are proved for actual smooth compactly supported physical coefficient extensions; no symbol/asymptotic identification is assumed.

def OAI.ElasticityBoundaryTaylor.line line 16
lemma OAI.ElasticityBoundaryTaylor.line_apply line 18
lemma OAI.ElasticityBoundaryTaylor.iteratedDeriv_line line 20
def OAI.ElasticityBoundaryTaylor.radialTaylor line 30
lemma OAI.ElasticityBoundaryTaylor.radialTaylor_eq_line line 34
lemma OAI.ElasticityBoundaryTaylor.radialTaylor_remainder line 46
lemma OAI.ElasticityBoundaryTaylor.compact_iteratedFDeriv_bound line 63
theorem OAI.ElasticityBoundaryTaylor.compact_radialTaylor_remainder line 73
Source documentation
Every smooth compactly supported coefficient has a global polynomially weighted Taylor remainder estimate, at every finite order.
```
theorem compact_radialTaylor_remainder {f : E → F} (hf : ContDiff ℝ (⊤ : ℕ∞) f)
    (hc : HasCompactSupport f) (n : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ z,
      ‖f z - radialTaylor f n z‖ ≤ C * ‖z‖^(n+1) := by
…
```
Mentions: OAI.ElasticityBoundaryTaylor.radialTaylor
abbrev OAI.ElasticityBoundaryTaylorPolynomial.Y line 92
def OAI.ElasticityBoundaryTaylorPolynomial.diagonal line 95
Source documentation
The diagonal of a real multilinear map, expanded in the fixed coordinates.
```
def diagonal {n : ℕ} (T : ContinuousMultilinearMap ℝ (fun _ : Fin n => Y) ℂ) : MP :=
…
```
Mentions: OAI.ElasticityBoundaryTaylorPolynomial.Y
lemma OAI.ElasticityBoundaryTaylorPolynomial.value_diagonal line 98
def OAI.ElasticityBoundaryTaylorPolynomial.taylor line 115
lemma OAI.ElasticityBoundaryTaylorPolynomial.value_taylor line 118
def OAI.ElasticityBoundaryTaylorPolynomial.weightOrder line 127
def OAI.ElasticityBoundaryTaylorPolynomial.parameterize line 129
lemma OAI.ElasticityBoundaryTaylorPolynomial.eval_parameterize line 132
lemma OAI.ElasticityBoundaryTaylorPolynomial.value_parameterize line 146
lemma OAI.ElasticityBoundaryTaylorPolynomial.value_parameterized_taylor line 156
lemma OAI.ElasticityBoundaryActualTower.operator_monomial line 173
def OAI.ElasticityBoundaryActualTower.amplitude line 180
lemma OAI.ElasticityBoundaryActualTower.coefficient_operator_amplitude line 183

theorem OAI.ElasticityBoundaryActualTower.finite_tensor_amplitude line 207

Source documentation

A true finite polynomial family cancels the literal tensor operator to any requested order. This is not an assumption about an unknown symbol.

theorem finite_tensor_amplitude (a : Tensor) (b : Lower) (l m : ℂ)
    (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0)
    (ha : ∀ i α j β, (a i α j β).coeff 0=C (ElasticityBoundaryLayerOperator.elasticityTensor l m i α j β))
    (p₀ : W) (h₀ : normal l m p₀=0) (N : ℕ) :
    ∃ (p : ℕ → W) (R : Polynomial W), p 0=p₀ ∧
      (∀ n, 0<n → boundary (p n)=0) ∧
      operator a b (amplitude p N)=Polynomial.X^(N+1)*R := by
…

Mentions: OAI.ElasticityBoundaryLayerOperator.elasticityTensor, OAI.ElasticityBoundaryActualTower.amplitude

lemma OAI.ElasticityBoundaryActualTower.parameterize_coeff_zero line 223
lemma OAI.ElasticityBoundaryActualTower.taylor_coeff_zero line 235
abbrev OAI.ElasticityBoundaryProfileBounds.Y line 257
def OAI.ElasticityBoundaryProfileBounds.halfspace line 259
lemma OAI.ElasticityBoundaryProfileBounds.measurable_halfspace line 260
lemma OAI.ElasticityBoundaryProfileBounds.one_add_pow_le line 263
lemma OAI.ElasticityBoundaryProfileBounds.polynomial_square_bound line 274
lemma OAI.ElasticityBoundaryProfileBounds.integrable_polynomial_square_weight line 285
lemma OAI.ElasticityBoundaryProfileBounds.integrableOn_profile_square line 297
lemma OAI.ElasticityBoundaryProfileBounds.memLp_profile line 304
lemma OAI.ElasticityBoundaryProfileBounds.integral_profile_square line 308
lemma OAI.ElasticityBoundaryProfileBounds.scale_mem_halfspace line 313
lemma OAI.ElasticityBoundaryProfileBounds.scale_indicator line 318
theorem OAI.ElasticityBoundaryProfileBounds.integralOn_scale line 326
lemma OAI.ElasticityBoundaryProfileBounds.integrableOn_scaled_iff line 332
lemma OAI.ElasticityBoundaryProfileBounds.physicalProfile_scale line 337
theorem OAI.ElasticityBoundaryProfileBounds.integral_physicalProfile_square line 342
Source documentation
Exact delta^4 factor in the true unscaled L2 mass.
```
theorem integral_physicalProfile_square {δ : ℝ} (hδ : δ≠0) (p : MP) :
    (∫ y in halfspace, ‖physicalProfile δ p y‖^2) =
      δ^4 * ∫ y : Y, ‖value p y‖^2*weight 2 y := by
…
```
Mentions: OAI.ElasticityBoundaryProfileBounds.halfspace, OAI.ElasticityBoundaryProfileBounds.Y
lemma OAI.ElasticityBoundaryProfileBounds.memLp_physicalProfile line 350
abbrev OAI.ElasticityBoundaryParameterBounds.Y line 370
def OAI.ElasticityBoundaryParameterBounds.atParameter line 372
lemma OAI.ElasticityBoundaryParameterBounds.atParameter_add line 374
lemma OAI.ElasticityBoundaryParameterBounds.value_parameter_monomial line 377
lemma OAI.ElasticityBoundaryParameterBounds.parameterGrowth line 381
lemma OAI.ElasticityBoundaryParameterBounds.parameter_square_bound line 405
lemma OAI.ElasticityBoundaryParameterBounds.parameter_mass_bound line 417
lemma OAI.ElasticityBoundaryParameterBounds.integral_physical_partial line 435
Source documentation
No inverse powers remain in the true L2 norm of a first physical partial: the inverse delta^4 differential factor and delta^4 Jacobian cancel exactly.
```
lemma integral_physical_partial {δ : ℝ} (hδ : δ≠0) (p : MP) (j : Fin 3) :
    (∫ z in halfspace, ‖fderiv ℝ (physicalProfile δ p) z (Pi.single j 1)‖^2) =
      ∫ y : Y, ‖value (D δ j p) y‖^2*weight 2 y := by
…
```
Mentions: OAI.ElasticityBoundaryParameterBounds.Y
theorem OAI.ElasticityBoundaryParameterBounds.uniform_physical_partial line 446
Source documentation
The actual corrected physical profiles, for a fixed finite polynomial family, have uniformly bounded first-partial L2 masses.
```
theorem uniform_physical_partial (q : Polynomial MP) (j : Fin 3) :
    ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 →
      (∫ z in halfspace, ‖fderiv ℝ (physicalProfile δ (atParameter q δ)) z
        (Pi.single j 1)‖^2) ≤ C := by
…
```
Mentions: OAI.ElasticityBoundaryParameterBounds.atParameter
abbrev OAI.ElasticityBoundaryOrderBound.Y line 471
def OAI.ElasticityBoundaryOrderBound.OrderBound line 476
Source documentation
A quantitative bound, with constants independent of concentration and of the half-space point. The polynomial spatial weight is integrable against our Gaussian/normal exponential.
```
def OrderBound (f : ℝ → Y → ℂ) (k : ℕ) : Prop :=
…
```
Mentions: OAI.ElasticityBoundaryOrderBound.Y
lemma OAI.ElasticityBoundaryOrderBound.OrderBound.zero line 480
lemma OAI.ElasticityBoundaryOrderBound.OrderBound.add line 483
lemma OAI.ElasticityBoundaryOrderBound.OrderBound.sum line 500
lemma OAI.ElasticityBoundaryOrderBound.OrderBound.mul line 509
lemma OAI.ElasticityBoundaryOrderBound.OrderBound.weaken line 521
lemma OAI.ElasticityBoundaryOrderBound.parameter_bound line 528
lemma OAI.ElasticityBoundaryOrderBound.power_bound line 533
lemma OAI.ElasticityBoundaryOrderBound.parameter_factor_bound line 537
lemma OAI.ElasticityBoundaryOrderBound.taylor_error_bound line 544
Source documentation
The actual smooth coefficient minus its literal Taylor polynomial carries the prescribed power of delta uniformly, not only at each fixed spatial point.
```
lemma taylor_error_bound {f : Y → ℂ} (hf : ContDiff ℝ (⊤ : ℕ∞) f)
    (hc : HasCompactSupport f) (N : ℕ) :
    OrderBound (fun δ y => f (scale δ y)-
      value (atParameter (parameterize (taylor f N)) δ) y) (N+1) := by
…
```
Mentions: OAI.ElasticityBoundaryOrderBound.Y, OAI.ElasticityBoundaryOrderBound.OrderBound

theorem OAI.ElasticityBoundaryOrderBound.OrderBound.square_mass line 561

Source documentation

Every such explicit bound gives a genuine weighted L2 estimate.

theorem OrderBound.square_mass {f : ℝ → Y → ℂ} {k : ℕ} (hf : OrderBound f k)
    (hm : ∀ δ, Continuous (f δ)) {b : ℝ} (hb : 0<b) :
    ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 →
      Integrable (fun y => ‖f δ y‖^2*weight b y) ∧
      (∫ y, ‖f δ y‖^2*weight b y) ≤ C*δ^(2*k) := by
…

Mentions: OAI.ElasticityBoundaryOrderBound.Y, OAI.ElasticityBoundaryOrderBound.OrderBound

abbrev OAI.ElasticityBoundarySmoothOperator.Y line 614
abbrev OAI.ElasticityBoundarySmoothOperator.SmoothTensor line 615
abbrev OAI.ElasticityBoundarySmoothOperator.SmoothLower line 616
def OAI.ElasticityBoundarySmoothOperator.tensorTaylor line 618
def OAI.ElasticityBoundarySmoothOperator.lowerTaylor line 620
def OAI.ElasticityBoundarySmoothOperator.scaledOperator line 625
Source documentation
The scaled amplitude of the literal differential expression; the PD operators are already identified with true scaled first/second derivatives.
```
def scaledOperator (a : SmoothTensor) (b : SmoothLower) (q : Polynomial W)
    (δ : ℝ) (i : Fin 3) (y : Y) : ℂ :=
…
```
Mentions: OAI.ElasticityBoundarySmoothOperator.SmoothTensor, OAI.ElasticityBoundarySmoothOperator.SmoothLower, OAI.ElasticityBoundarySmoothOperator.Y
lemma OAI.ElasticityBoundarySmoothOperator.polynomial_operator_value line 632
def OAI.ElasticityBoundarySmoothOperator.scaledError line 642
lemma OAI.ElasticityBoundarySmoothOperator.scaledOperator_decomposition line 651
lemma OAI.ElasticityBoundarySmoothOperator.error_order_bound line 660
lemma OAI.ElasticityBoundarySmoothOperator.unpack_X_pow_mul line 689
lemma OAI.ElasticityBoundarySmoothOperator.scaledOperator_order_bound line 693
lemma OAI.ElasticityBoundarySmoothOperator.continuous_scaledOperator line 702

theorem OAI.ElasticityBoundarySmoothOperator.finite_smooth_amplitude line 723

Source documentation

For every smooth compact coefficient tensor with the physical frozen value, the constructed amplitudes have a genuine arbitrarily small scaled residual in weighted L2. No near-constantness is required.

theorem finite_smooth_amplitude (a : SmoothTensor) (b : SmoothLower)
    (ha : ∀ i α j β, ContDiff ℝ (⊤ : ℕ∞) (a i α j β) ∧ HasCompactSupport (a i α j β))
    (hb : ∀ i j β, ContDiff ℝ (⊤ : ℕ∞) (b i j β) ∧ HasCompactSupport (b i j β))
    (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0)
    (ha0 : ∀ i α j β, a i α j β 0=elasticityTensor l m i α j β)
    (p₀ : W) (h₀ : normal l m p₀=0) (N : ℕ) :
    ∃ p : ℕ → W, p 0=p₀ ∧ (∀ n, 0<n → boundary (p n)=0) ∧
      ∀ i : Fin 3, ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 →
        Integrable (fun y => ‖scaledOperator a b (amplitude p N) δ i y‖^2*weight 2 y) ∧
        (∫ y, ‖scaledOperator a b (amplitude p N) δ i y‖^2*weight 2 y) ≤ C*δ^(2*(N+1)) := by
…

Mentions: OAI.ElasticityBoundarySmoothOperator.SmoothTensor, OAI.ElasticityBoundarySmoothOperator.SmoothLower, OAI.ElasticityBoundarySmoothOperator.scaledOperator

abbrev OAI.ElasticityBoundaryStrongLayer.Y line 759
def OAI.ElasticityBoundaryStrongLayer.dpart line 761
def OAI.ElasticityBoundaryStrongLayer.strong line 764
def OAI.ElasticityBoundaryStrongLayer.layer line 768
lemma OAI.ElasticityBoundaryStrongLayer.D_atParameter line 771
lemma OAI.ElasticityBoundaryStrongLayer.partial_layer line 774
lemma OAI.ElasticityBoundaryStrongLayer.second_layer line 779
theorem OAI.ElasticityBoundaryStrongLayer.strong_layer_scale line 788
Source documentation
The computed scaled operator is exactly the actual strong differential residual, including all coefficient-gradient/lower terms.
```
theorem strong_layer_scale (a : SmoothTensor) (b : SmoothLower)
    {δ : ℝ} (hδ : δ≠0) (q : Polynomial W) (i : Fin 3) (y : Y) :
    strong a b (layer q δ) i (scale δ y) =
      ((δ^4)⁻¹:ℝ) • (envelope δ y*scaledOperator a b q δ i y) := by
…
```
Mentions: OAI.ElasticityBoundaryStrongLayer.Y, OAI.ElasticityBoundaryStrongLayer.strong, OAI.ElasticityBoundaryStrongLayer.layer
lemma OAI.ElasticityBoundaryStrongLayer.envelope_product_indicator line 806
lemma OAI.ElasticityBoundaryStrongLayer.integral_envelope_product line 814
lemma OAI.ElasticityBoundaryStrongLayer.integrable_envelope_product_iff line 819
lemma OAI.ElasticityBoundaryStrongLayer.strong_layer_mass line 827
lemma OAI.ElasticityBoundaryStrongLayer.integrable_strong_layer_square line 840
lemma OAI.ElasticityBoundaryStrongLayer.continuous_strong_layer line 848

theorem OAI.ElasticityBoundaryStrongLayer.finite_strong_layer line 876

Source documentation

Genuine arbitrary-order half-space strong residuals of finite smooth boundary trial fields. The norm is the actual unscaled L2 norm.

theorem finite_strong_layer (a : SmoothTensor) (b : SmoothLower)
    (ha : ∀ i α j β, ContDiff ℝ (⊤ : ℕ∞) (a i α j β) ∧ HasCompactSupport (a i α j β))
    (hb : ∀ i j β, ContDiff ℝ (⊤ : ℕ∞) (b i j β) ∧ HasCompactSupport (b i j β))
    (l m : ℂ) (hm : m≠0) (he : l+2*m≠0) (hp : l+3*m≠0)
    (ha0 : ∀ i α j β, a i α j β 0=elasticityTensor l m i α j β)
    (p₀ : W) (h₀ : normal l m p₀=0) (N : ℕ) :
    ∃ p : ℕ → W, p 0=p₀ ∧ (∀ n, 0<n → boundary (p n)=0) ∧
      ∀ i : Fin 3, ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 →
        MemLp (strong a b (layer (amplitude p (N+1)) δ) i) 2 (volume.restrict halfspace) ∧
        (∫ z in halfspace, ‖strong a b (layer (amplitude p (N+1)) δ) i z‖^2) ≤ C*δ^(2*N) := by
…

Mentions: OAI.ElasticityBoundaryStrongLayer.strong, OAI.ElasticityBoundaryStrongLayer.layer

abbrev OAI.ElasticityBoundaryPullback.I line 914
abbrev OAI.ElasticityBoundaryPullback.Y line 915
abbrev OAI.ElasticityBoundaryPullback.Tensor line 917
abbrev OAI.ElasticityBoundaryPullback.Lower line 918
def OAI.ElasticityBoundaryPullback.directional line 920
def OAI.ElasticityBoundaryPullback.principalPull line 924
def OAI.ElasticityBoundaryPullback.lowerPull line 927
lemma OAI.ElasticityBoundaryPullback.shuffle3 line 931
lemma OAI.ElasticityBoundaryPullback.shuffle5 line 938
theorem OAI.ElasticityBoundaryPullback.directional_comp line 955
Source documentation
The actual system under a smooth coordinate map, including all lower terms from its Hessian. No coordinate Jacobian is silently discarded.
```
theorem directional_comp (e : I → E) (a : Tensor E) (b : Lower E)
    {ψ : E → Y} (hψ : ContDiff ℝ (⊤ : ℕ∞) ψ) (u : I → Y → ℂ)
    (hu : ∀ j, ContDiff ℝ (⊤ : ℕ∞) (u j)) (i : I) (x : E) :
    directional e a b (fun j z => u j (ψ z)) i x =
      (∑ α, ∑ j, ∑ β, principalPull e a ψ i α j β x*cp (cp (u j) β) α (ψ x))+
        ∑ j, ∑ β, lowerPull e a b ψ i j β x*cp (u j) β (ψ x) := by
…
```
Mentions: OAI.ElasticityBoundaryPullback.I, OAI.ElasticityBoundaryPullback.Tensor, OAI.ElasticityBoundaryPullback.Lower, OAI.ElasticityBoundaryPullback.Y, OAI.ElasticityBoundaryPullback.directional, OAI.ElasticityBoundaryPullback.principalPull, OAI.ElasticityBoundaryPullback.lowerPull
abbrev OAI.ElasticityBoundaryRotation.I line 1010
abbrev OAI.ElasticityBoundaryRotation.X line 1011
def OAI.ElasticityBoundaryRotation.frameMatrix line 1013
lemma OAI.ElasticityBoundaryRotation.frameMatrix_orthogonal line 1015
def OAI.ElasticityBoundaryRotation.rotateTensor line 1028
def OAI.ElasticityBoundaryRotation.columnDot line 1031
lemma OAI.ElasticityBoundaryRotation.rotate_isotropic_formula line 1033
theorem OAI.ElasticityBoundaryRotation.rotate_isotropic line 1066
Source documentation
Simultaneously transporting displacement and spatial coordinates by the same actual orthogonal frame leaves the frozen physical tensor unchanged.
```
theorem rotate_isotropic (Q : X ≃ₗᵢ[ℝ] X) (l m : ℂ) (s α r β : I) :
    rotateTensor (frameMatrix Q) (elasticityTensor l m) s α r β=elasticityTensor l m s α r β := by
…
```
Mentions: OAI.ElasticityBoundaryRotation.X, OAI.ElasticityBoundaryRotation.I, OAI.ElasticityBoundaryRotation.rotateTensor, OAI.ElasticityBoundaryRotation.frameMatrix
abbrev OAI.ElasticityBoundaryFrameOperator.I line 1081
def OAI.ElasticityBoundaryFrameOperator.mix line 1084
def OAI.ElasticityBoundaryFrameOperator.mixedTensor line 1086
def OAI.ElasticityBoundaryFrameOperator.mixedLower line 1089
lemma OAI.ElasticityBoundaryFrameOperator.smooth_mix line 1092
lemma OAI.ElasticityBoundaryFrameOperator.dd_mix line 1097
lemma OAI.ElasticityBoundaryFrameOperator.dd_dd_mix line 1109
lemma OAI.ElasticityBoundaryFrameOperator.shuffle4 line 1118
theorem OAI.ElasticityBoundaryFrameOperator.directional_mix line 1129
Source documentation
Input displacement and output equation rotation retain every literal term.
```
theorem directional_mix (e : I → E) (R S : I → I → ℂ) (a : Tensor E) (b : Lower E)
    (u : I → E → ℂ) (hu : ∀ j, ContDiff ℝ (⊤ : ℕ∞) (u j)) (s : I) (x : E) :
    (∑ i, R s i*directional e a b (mix S u) i x)=
      directional e (mixedTensor R S a) (mixedLower R S b) u s x := by
…
```
Mentions: OAI.ElasticityBoundaryFrameOperator.I, OAI.ElasticityBoundaryFrameOperator.mix, OAI.ElasticityBoundaryFrameOperator.mixedTensor, OAI.ElasticityBoundaryFrameOperator.mixedLower
abbrev OAI.ElasticityBoundaryPhysicalStrong.I line 1173
def OAI.ElasticityBoundaryPhysicalStrong.divergence line 1176
def OAI.ElasticityBoundaryPhysicalStrong.stress line 1178
def OAI.ElasticityBoundaryPhysicalStrong.coeff line 1182
def OAI.ElasticityBoundaryPhysicalStrong.lower line 1184
lemma OAI.ElasticityBoundaryPhysicalStrong.dd_add line 1188
lemma OAI.ElasticityBoundaryPhysicalStrong.dd_ite line 1193
lemma OAI.ElasticityBoundaryPhysicalStrong.smooth_divergence line 1197
lemma OAI.ElasticityBoundaryPhysicalStrong.stress_derivative line 1201
lemma OAI.ElasticityBoundaryPhysicalStrong.tensor_contract line 1228
lemma OAI.ElasticityBoundaryPhysicalStrong.lower_contract line 1237
theorem OAI.ElasticityBoundaryPhysicalStrong.stress_divergence line 1247
Source documentation
Divergence of the physical Lamé stress equals the constructed literal second-order system, including its exact first-order coefficient terms.
```
theorem stress_divergence (e : I → E) {l m : E → ℂ}
    (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (u : I → E → ℂ) (hu : ∀ j, ContDiff ℝ (⊤ : ℕ∞) (u j)) (i : I) (x : E) :
    (∑ k, dd (stress e l m u i k) (e k) x)=directional e (coeff l m) (lower e l m) u i x := by
…
```
Mentions: OAI.ElasticityBoundaryPhysicalStrong.I, OAI.ElasticityBoundaryPhysicalStrong.stress, OAI.ElasticityBoundaryPhysicalStrong.coeff, OAI.ElasticityBoundaryPhysicalStrong.lower