BoundaryParametrix.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

Physical displacements obtained from compact chart fields. Their literal strong Lamé force is the constructed curved-coordinate operator on the whole trial support, rather than a formally equated auxiliary DN system.

abbrev OAI.ElasticityBoundaryPhysicalTransfer.I line 16
abbrev OAI.ElasticityBoundaryPhysicalTransfer.X line 17
abbrev OAI.ElasticityBoundaryPhysicalTransfer.Y line 18
def OAI.ElasticityBoundaryPhysicalTransfer.lifted line 20
def OAI.ElasticityBoundaryPhysicalTransfer.transferred line 23
def OAI.ElasticityBoundaryPhysicalTransfer.force line 27
lemma OAI.ElasticityBoundaryPhysicalTransfer.smooth_lifted line 30
lemma OAI.ElasticityBoundaryPhysicalTransfer.smooth_transferred line 35
lemma OAI.ElasticityBoundaryPhysicalTransfer.support_lifted line 43
lemma OAI.ElasticityBoundaryPhysicalTransfer.support_transferred line 55
lemma OAI.ElasticityBoundaryPhysicalTransfer.transferred_germ line 61
lemma OAI.ElasticityBoundaryPhysicalTransfer.chart_force line 70

theorem OAI.ElasticityBoundaryPhysicalTransfer.transferred_force line 89

Source documentation

The exact coordinate operator controls the genuine transferred physical force at every point of the compact trial support.

theorem transferred_force (e : OpenPartialHomeomorph X X) {K : Set X}
    (hK : K⊆e.source) {η : X → ℝ} (hη : ∀ z∈e '' K, η z=1)
    (Q : X ≃ₗᵢ[ℝ] X) (u : I → Y → ℂ)
    (hus : ∀ j, Function.support (fun z : X => u j z.ofLp)⊆K)
    (hu : ∀ j, ContDiff ℝ (⊤ : ℕ∞) (u j))
    (Φ Ψ : X → X) (hΨ : ContDiff ℝ (⊤ : ℕ∞) Ψ)
    {l m : X → ℂ} (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (y : Y) (hy : WithLp.toLp 2 y∈K)
    (hΦy : Φ (WithLp.toLp 2 y)=e (WithLp.toLp 2 y))
    (hΨy : Ψ =ᶠ[𝓝 (e (WithLp.toLp 2 y))] e.symm) (s : I) :
    (∑ i, frameMatrix Q i s*force l m (transferred e η Q u) i (e (WithLp.toLp 2 y)))=
      strong (chartPrincipal Q (fun z => Φ (WithLp.toLp 2 z)) (fun z => (Ψ z).ofLp) l m)
…

Mentions: OAI.ElasticityBoundaryPhysicalTransfer.X, OAI.ElasticityBoundaryPhysicalTransfer.I, OAI.ElasticityBoundaryPhysicalTransfer.Y, OAI.ElasticityBoundaryPhysicalTransfer.force, OAI.ElasticityBoundaryPhysicalTransfer.transferred

abbrev OAI.ElasticityBoundaryCutoffBound.Y line 129
lemma OAI.ElasticityBoundaryCutoffBound.bounded_scaled line 131
lemma OAI.ElasticityBoundaryCutoffBound.compact_scaled line 135
theorem OAI.ElasticityBoundaryCutoffBound.flat_scaled line 143
Source documentation
A bounded coefficient vanishing on a fixed neighborhood of the base point yields every power of the true concentration parameter.
```
theorem flat_scaled {f : Y → ℂ} {M r : ℝ} (hM : 0≤M) (hr : 0<r)
    (hf : ∀ y, ‖f y‖≤M) (hz : ∀ y, ‖y‖<r → f y=0) (N : ℕ) :
    OrderBound (fun δ y => f (scale δ y)) N := by
…
```
Mentions: OAI.ElasticityBoundaryCutoffBound.Y
lemma OAI.ElasticityBoundaryCutoffBound.compact_flat_scaled line 161
abbrev OAI.ElasticityBoundaryCutoffLayer.Y line 188
lemma OAI.ElasticityBoundaryCutoffLayer.smooth_dpart line 190
lemma OAI.ElasticityBoundaryCutoffLayer.compact_dpart line 194
lemma OAI.ElasticityBoundaryCutoffLayer.dpart_eventually_zero line 197
lemma OAI.ElasticityBoundaryCutoffLayer.dpart_mul line 202
lemma OAI.ElasticityBoundaryCutoffLayer.second_mul line 209
def OAI.ElasticityBoundaryCutoffLayer.cutoffCorrection line 224
Source documentation
All cutoff product terms, before taking an absolute value or norm.
```
def cutoffCorrection (a : SmoothTensor) (b : SmoothLower) (χ : Y → ℂ)
    (q : Polynomial W) (δ : ℝ) (i : Fin 3) (y : Y) : ℂ :=
…
```
Mentions: OAI.ElasticityBoundaryCutoffLayer.Y
def OAI.ElasticityBoundaryCutoffLayer.cutoffScaled line 234
lemma OAI.ElasticityBoundaryCutoffLayer.correction_order_bound line 238
def OAI.ElasticityBoundaryCutoffLayer.cutoffLayer line 285
lemma OAI.ElasticityBoundaryCutoffLayer.smooth_cutoffLayer line 288
lemma OAI.ElasticityBoundaryCutoffLayer.compact_cutoffLayer line 293
lemma OAI.ElasticityBoundaryCutoffLayer.first_cutoff line 297
lemma OAI.ElasticityBoundaryCutoffLayer.second_cutoff line 303

theorem OAI.ElasticityBoundaryCutoffLayer.strong_cutoff_scale line 311

Source documentation

Literal product-rule residual of the localized physical boundary layer.

theorem strong_cutoff_scale (a : SmoothTensor) (b : SmoothLower)
    {χ : Y → ℂ} (hχ : ContDiff ℝ (⊤ : ℕ∞) χ)
    {δ : ℝ} (hδ : δ≠0) (q : Polynomial W) (i : Fin 3) (y : Y) :
    strong a b (cutoffLayer χ q δ) i (scale δ y) =
      ((δ^4)⁻¹:ℝ) • (envelope δ y*cutoffScaled a b χ q δ i y) := by
…

Mentions: OAI.ElasticityBoundaryCutoffLayer.Y, OAI.ElasticityBoundaryCutoffLayer.cutoffLayer, OAI.ElasticityBoundaryCutoffLayer.cutoffScaled

lemma OAI.ElasticityBoundaryCutoffLayer.continuous_cutoffScaled line 335
abbrev OAI.ElasticityBoundaryCutoffParametrix.Y line 388
lemma OAI.ElasticityBoundaryCutoffParametrix.scaled_envelope_mass line 390
lemma OAI.ElasticityBoundaryCutoffParametrix.scaled_envelope_integrable line 398
lemma OAI.ElasticityBoundaryCutoffParametrix.continuous_strong line 406

theorem OAI.ElasticityBoundaryCutoffParametrix.finite_cutoff_layer line 425

Source documentation

A localized smooth physical trial field with arbitrary small strong force.

theorem finite_cutoff_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 β))
    {χ : Y → ℂ} (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hc : HasCompactSupport χ)
    (hχ0 : χ =ᶠ[𝓝 (0:Y)] fun _ => 1)
    (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 (cutoffLayer χ (amplitude p (N+1)) δ) i) 2 (volume.restrict halfspace) ∧
        (∫ z in halfspace, ‖strong a b (cutoffLayer χ (amplitude p (N+1)) δ) i z‖^2) ≤ C*δ^(2*N) := by
…

Mentions: OAI.ElasticityBoundaryCutoffParametrix.Y

def OAI.ElasticityBoundaryCutoffParametrix.firstScaled line 469
Source documentation
Amplitude of a genuine first derivative, including the cutoff derivative.
```
def firstScaled (χ : Y → ℂ) (q : Polynomial W) (δ : ℝ) (j β : Fin 3) (y : Y) : ℂ :=
…
```
Mentions: OAI.ElasticityBoundaryCutoffParametrix.Y
lemma OAI.ElasticityBoundaryCutoffParametrix.first_scaled_identity line 473
lemma OAI.ElasticityBoundaryCutoffParametrix.first_scaled_bound line 484
lemma OAI.ElasticityBoundaryCutoffParametrix.first_scaled_continuous line 496

theorem OAI.ElasticityBoundaryCutoffParametrix.cutoff_gradient_bound line 504

Source documentation

The actual physical gradient is uniformly L2 bounded; its delta^-2 factor is canceled by the genuine anisotropic delta^4 volume factor.

theorem cutoff_gradient_bound {χ : Y → ℂ} (hχ : ContDiff ℝ (⊤ : ℕ∞) χ)
    (hc : HasCompactSupport χ) (q : Polynomial W) (j β : Fin 3) :
    ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 →
      MemLp (dpart (cutoffLayer χ q δ j) β) 2 (volume.restrict halfspace) ∧
      (∫ z in halfspace, ‖dpart (cutoffLayer χ q δ j) β z‖^2) ≤ C := by
…

Mentions: OAI.ElasticityBoundaryCutoffParametrix.Y

abbrev OAI.ElasticityBoundaryLocalParametrix.I line 539
abbrev OAI.ElasticityBoundaryLocalParametrix.Y line 540
lemma OAI.ElasticityBoundaryLocalParametrix.strong_support line 542
lemma OAI.ElasticityBoundaryLocalParametrix.strong_mul_coeff line 547
lemma OAI.ElasticityBoundaryLocalParametrix.localize_strong line 553
lemma OAI.ElasticityBoundaryLocalParametrix.cutoff_support line 566
lemma OAI.ElasticityBoundaryLocalParametrix.compact_coefficients line 573

theorem OAI.ElasticityBoundaryLocalParametrix.finite_local_layer line 602

Source documentation

The true arbitrary-order strong quasimode theorem needs only local smoothness of the physical pullback. Compact coefficients used during the Taylor construction leave the literal final operator unchanged.

theorem finite_local_layer (a : SmoothTensor) (b : SmoothLower)
    (ha : ∀ i α j β, ContDiff ℝ (⊤ : ℕ∞) (a i α j β))
    (hb : ∀ i j β, ContDiff ℝ (⊤ : ℕ∞) (b i j β))
    {χ : Y → ℂ} (hχ : ContDiff ℝ (⊤ : ℕ∞) χ) (hc : HasCompactSupport χ)
    (hχ0 : χ =ᶠ[𝓝 (0:Y)] fun _ => 1)
    (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 : I, ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 →
        MemLp (strong a b (cutoffLayer χ (amplitude p (N+1)) δ) i) 2 (volume.restrict halfspace) ∧
        (∫ z in halfspace, ‖strong a b (cutoffLayer χ (amplitude p (N+1)) δ) i z‖^2) ≤ C*δ^(2*N) := by
…

Mentions: OAI.ElasticityBoundaryLocalParametrix.Y, OAI.ElasticityBoundaryLocalParametrix.I