BoundaryPackets.lean`

90 declarations, 0 contain sorry, 0 declared as axioms

The exact inverse derivative at normalized physical boundary charts.

abbrev OAI.ElasticityBoundaryInverseGeometry.I line 13
abbrev OAI.ElasticityBoundaryInverseGeometry.X line 14
abbrev OAI.ElasticityBoundaryInverseGeometry.Y line 15
lemma OAI.ElasticityBoundaryInverseGeometry.inverse_derivative line 17
lemma OAI.ElasticityBoundaryInverseGeometry.inverse_frame_entry line 37
lemma OAI.ElasticityBoundaryInverseGeometry.coordinate_inverse_jac line 43
abbrev OAI.ElasticityBoundaryFrameInverse.I line 70
abbrev OAI.ElasticityBoundaryFrameInverse.X line 71
lemma OAI.ElasticityBoundaryFrameInverse.frameMatrix_symm line 73
lemma OAI.ElasticityBoundaryFrameInverse.frameMatrix_rows line 77
lemma OAI.ElasticityBoundaryFrameInverse.frame_inverse line 81
lemma OAI.ElasticityBoundaryFrameInverse.norm_sq_sum_three line 88
lemma OAI.ElasticityBoundaryFrameInverse.norm_frame_entry line 96
lemma OAI.ElasticityBoundaryFrameInverse.physical_component_bound line 100
abbrev OAI.ElasticityBoundaryForceSupport.I line 126
abbrev OAI.ElasticityBoundaryForceSupport.X line 127
abbrev OAI.ElasticityBoundaryForceSupport.Y line 128
lemma OAI.ElasticityBoundaryForceSupport.compact_image line 130
lemma OAI.ElasticityBoundaryForceSupport.force_support line 134
lemma OAI.ElasticityBoundaryForceSupport.transferred_force_support line 139
lemma OAI.ElasticityBoundaryForceSupport.strong_support_lifted line 146

theorem OAI.ElasticityBoundaryForceSupport.transferred_force_all line 159

Source documentation

No operator identity is required outside the actual support: locality proves both sides vanish there.

theorem transferred_force_all (e : OpenPartialHomeomorph X X) {K : Set X}
    (hK : IsCompact K) (hs : K⊆e.source) {η : X → ℝ} (hηs : tsupport η⊆e.target)
    (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 ℝ (⊤ : ℕ∞) Ψ)
    (hΦ : ∀ y∈K, Φ y=e y) (hΨe : ∀ z∈e '' K, Ψ =ᶠ[𝓝 z] e.symm)
    {l m : X → ℂ} (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (x : X) (hx : x∈e.source) (s : I) :
    (∑ i, frameMatrix Q i s*force l m (transferred e η Q u) i (e x))=
      strong (chartPrincipal Q (fun z => Φ (WithLp.toLp 2 z)) (fun z => (Ψ z).ofLp) l m)
        (chartLower Q (fun z => Φ (WithLp.toLp 2 z)) (fun z => (Ψ z).ofLp) l m) u s x.ofLp := by
…

Mentions: OAI.ElasticityBoundaryForceSupport.X, OAI.ElasticityBoundaryForceSupport.I, OAI.ElasticityBoundaryForceSupport.Y

theorem OAI.ElasticityBoundaryChartIntegral.compact_chart_integral line 202

Source documentation

A compactly supported physical integrand pulls back with its exact Jacobian, including the domain's half-space indicator.

theorem compact_chart_integral (e : OpenPartialHomeomorph E E)
    (he : ContDiffOn ℝ (⊤ : ℕ∞) e e.source)
    {K Ω H : Set E} (hs : K⊆e.source) (hΩ : MeasurableSet Ω) (hH : MeasurableSet H)
    (hhalf : ∀ y∈e.source, e y∈Ω ↔ y∈H)
    {Φ : E → E} (hΦ : ∀ y∈K, Φ =ᶠ[𝓝 y] e)
    (f g : E → ℝ) (hf : Function.support f⊆e '' K) (hg : Function.support g⊆K)
    (hfg : ∀ y∈e.source, f (e y)=g y) :
    (∫ x in Ω, f x ∂μ)=(∫ y in H, |(fderiv ℝ Φ y).det| *g y ∂μ) := by
…

lemma OAI.ElasticityBoundaryChartIntegral.compact_abs_det_bound line 243

theorem OAI.ElasticityBoundaryChartIntegral.compact_jacobian_mass_bound line 253

Source documentation

The physical mass bound used for actual localized stress residuals.

theorem compact_jacobian_mass_bound {K H : Set E} (hK : IsCompact K)
    {Φ : E → E} (hΦ : ContDiff ℝ (⊤ : ℕ∞) Φ) :
    ∃ C : ℝ, 0≤C ∧ ∀ g : E → ℝ, Continuous g → HasCompactSupport g →
      Function.support g⊆K → (∀ y, 0≤g y) →
      (∫ y in H, |(fderiv ℝ Φ y).det| *g y ∂μ)≤C*(∫ y in H, g y ∂μ) := by
…

abbrev OAI.ElasticityBoundaryChartMass.I line 285
abbrev OAI.ElasticityBoundaryChartMass.X line 286
abbrev OAI.ElasticityBoundaryChartMass.Y line 287
def OAI.ElasticityBoundaryChartMass.inverseMix line 289
lemma OAI.ElasticityBoundaryChartMass.inverseMix_support line 292
lemma OAI.ElasticityBoundaryChartMass.inverseMix_bound line 303
lemma OAI.ElasticityBoundaryChartMass.norm_sq_integrableOn line 312

theorem OAI.ElasticityBoundaryChartMass.chart_frame_mass_bound line 323

Source documentation

Uniform transfer of the exact strong residual. There is no assumed physical/augmented DN equality and no suppressed determinant.

theorem chart_frame_mass_bound (e : OpenPartialHomeomorph X X)
    (he : ContDiffOn ℝ (⊤ : ℕ∞) e e.source)
    {K Ω H : Set X} (hK : IsCompact K) (hs : K⊆e.source)
    (hΩ : MeasurableSet Ω) (hH : MeasurableSet H)
    (hhalf : ∀ y∈e.source, e y∈Ω ↔ y∈H)
    {Φ : X → X} (hΦs : ContDiff ℝ (⊤ : ℕ∞) Φ) (hΦ : ∀ y∈K, Φ =ᶠ[𝓝 y] e)
    (Q : X ≃ₗᵢ[ℝ] X) :
    ∃ C : ℝ, 0≤C ∧ ∀ (f g : I → X → ℂ),
      (∀ i, Function.support (f i)⊆e '' K) →
      (∀ j, Continuous (g j)) → (∀ j, Function.support (g j)⊆K) →
      (∀ y∈e.source, ∀ s, (∑ i, frameMatrix Q i s*f i (e y))=g s y) →
      ∀ i, (∫ x in Ω, ‖f i x‖^2)≤C*∑ s, (∫ y in H, ‖g s y‖^2) := by
…

Mentions: OAI.ElasticityBoundaryChartMass.X, OAI.ElasticityBoundaryChartMass.I

lemma OAI.ElasticityBoundaryChartMass.integral_ofLp line 371
Source documentation
The coordinate product measure is the actual Euclidean volume, not a normalization chosen during the argument.
```
lemma integral_ofLp {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (g : Y → F) (H : Set Y) :
    (∫ x : X in (WithLp.ofLp ⁻¹' H), g x.ofLp)=(∫ y in H, g y) :=
…
```
Mentions: OAI.ElasticityBoundaryChartMass.Y, OAI.ElasticityBoundaryChartMass.X
abbrev OAI.ElasticityBoundaryPhysicalMass.I line 392
abbrev OAI.ElasticityBoundaryPhysicalMass.X line 393
abbrev OAI.ElasticityBoundaryPhysicalMass.Y line 394
lemma OAI.ElasticityBoundaryPhysicalMass.smooth_strong line 396
def OAI.ElasticityBoundaryPhysicalMass.principal line 405
def OAI.ElasticityBoundaryPhysicalMass.lower line 408

theorem OAI.ElasticityBoundaryPhysicalMass.transferred_mass_bound line 413

Source documentation

The multiplicative constant depends only on the fixed chart, not on the field, its frequency, or the chosen finite parametrix order.

theorem transferred_mass_bound (e : OpenPartialHomeomorph X X)
    (he : ContDiffOn ℝ (⊤ : ℕ∞) e e.source)
    {K Ω H : Set X} (hK : IsCompact K) (hs : K⊆e.source)
    (hΩ : MeasurableSet Ω) (hH : MeasurableSet H)
    (hhalf : ∀ y∈e.source, e y∈Ω ↔ y∈H)
    {η : X → ℝ} (hηs : tsupport η⊆e.target) (hη : ∀ z∈e '' K, η z=1)
    (Q : X ≃ₗᵢ[ℝ] X) (Φ Ψ : X → X)
    (hΦs : ContDiff ℝ (⊤ : ℕ∞) Φ) (hΨs : ContDiff ℝ (⊤ : ℕ∞) Ψ)
    (hΦ : ∀ y∈K, Φ =ᶠ[𝓝 y] e) (hΨ : ∀ z∈e '' K, Ψ =ᶠ[𝓝 z] e.symm)
    {l m : X → ℂ} (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    :
    ∃ C : ℝ, 0≤C ∧ ∀ (u : I → Y → ℂ),
…

Mentions: OAI.ElasticityBoundaryPhysicalMass.X, OAI.ElasticityBoundaryPhysicalMass.I, OAI.ElasticityBoundaryPhysicalMass.Y

abbrev OAI.ElasticityBoundaryCompactMatrix.I line 456
abbrev OAI.ElasticityBoundaryCompactMatrix.X line 457
lemma OAI.ElasticityBoundaryCompactMatrix.compact_array_bound line 459
def OAI.ElasticityBoundaryCompactMatrix.row line 472
lemma OAI.ElasticityBoundaryCompactMatrix.row_support line 474
lemma OAI.ElasticityBoundaryCompactMatrix.continuous_row line 484
lemma OAI.ElasticityBoundaryCompactMatrix.row_bound line 488
lemma OAI.ElasticityBoundaryCompactMatrix.row_mass_bound line 504
abbrev OAI.ElasticityBoundaryGradientTransfer.I line 530
abbrev OAI.ElasticityBoundaryGradientTransfer.X line 531
abbrev OAI.ElasticityBoundaryGradientTransfer.Y line 532
lemma OAI.ElasticityBoundaryGradientTransfer.frame_forward line 534
lemma OAI.ElasticityBoundaryGradientTransfer.dd_support line 538
lemma OAI.ElasticityBoundaryGradientTransfer.dpart_support_lifted line 544
def OAI.ElasticityBoundaryGradientTransfer.jacobian line 555
lemma OAI.ElasticityBoundaryGradientTransfer.smooth_jacobian line 558
lemma OAI.ElasticityBoundaryGradientTransfer.gradient_at_support line 564
lemma OAI.ElasticityBoundaryGradientTransfer.gradient_all line 589
abbrev OAI.ElasticityBoundaryGradientMass.I line 628
abbrev OAI.ElasticityBoundaryGradientMass.X line 629
abbrev OAI.ElasticityBoundaryGradientMass.Y line 630
lemma OAI.ElasticityBoundaryGradientMass.transferred_value line 632
lemma OAI.ElasticityBoundaryGradientMass.transferred_value_mass line 654
lemma OAI.ElasticityBoundaryGradientMass.transferred_gradient_mass line 666
abbrev OAI.ElasticityBoundaryPacket.I line 704
abbrev OAI.ElasticityBoundaryPacket.X line 705
abbrev OAI.ElasticityBoundaryPacket.Y line 706
structure OAI.ElasticityBoundaryPacket.Setup line 708
lemma OAI.ElasticityBoundaryPacket.setup_exists line 737
lemma OAI.ElasticityBoundaryPacket.Setup.zero_mem line 779
lemma OAI.ElasticityBoundaryPacket.Setup.Φ_zero line 785
lemma OAI.ElasticityBoundaryPacket.Setup.frozen line 788
abbrev OAI.ElasticityBoundaryPacketMass.I line 815
abbrev OAI.ElasticityBoundaryPacketMass.Y line 816
abbrev OAI.ElasticityBoundaryPacketMass.X line 817
def OAI.ElasticityBoundaryPacketMass.H line 819
lemma OAI.ElasticityBoundaryPacketMass.measurable_H line 820
lemma OAI.ElasticityBoundaryPacketMass.integral_ofLp line 824

lemma OAI.ElasticityBoundaryPacketMass.cutoff_value_bound line 833

Source documentation

The lower-order value term even decays as delta^4.

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

Mentions: OAI.ElasticityBoundaryPacketMass.Y, OAI.ElasticityBoundaryPacketMass.I

def OAI.Elasticity.physicalResidual line 872
Source documentation
The variational residual, acting on all zero-trace test fields.
```
def physicalResidual (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
    (u : H1Hilbert Ω) : H10Hilbert Ω →L[ℝ] ℝ :=
…
```
Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1Hilbert, OAI.Elasticity.H10Hilbert
def OAI.Elasticity.physicalProjection line 877
Source documentation
The actual physical solution with the same trace as the trial field.
```
def physicalProjection (u : H1Hilbert Ω) : H1Hilbert Ω :=
…
```
Mentions: OAI.Elasticity.H1Hilbert
lemma OAI.Elasticity.physicalProjection_weak line 880
lemma OAI.Elasticity.physicalProjection_trace line 886
def OAI.Elasticity.physicalError line 894
Source documentation
The exact zero-trace correction, not an assumed quasimode remainder.
```
def physicalError (ha : Admissible Ω lam mu) (hO : IsOpen Ω)
    (hB : Bornology.IsBounded Ω) (u : H1Hilbert Ω) : H10Hilbert Ω :=
…
```
Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.H1Hilbert, OAI.Elasticity.H10Hilbert
lemma OAI.Elasticity.error_residual line 900

theorem OAI.Elasticity.physicalError_bound line 913

Source documentation

Coercivity gives a uniform correction bound in the honest Hilbert norm.

theorem physicalError_bound (ha : Admissible Ω lam mu) (hO : IsOpen Ω)
    (hB : Bornology.IsBounded Ω) :
    ∃ c : ℝ, 0 < c ∧ ∀ u : H1Hilbert Ω,
      ‖physicalError ha hO hB u‖ ≤
      ‖physicalResidual (ha.1.boundedCoefficient hO hB) (ha.2.1.boundedCoefficient hO hB) u‖ / c := by
…

Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.H1Hilbert, OAI.Elasticity.physicalError, OAI.Elasticity.physicalResidual

theorem OAI.Elasticity.DN_quasimode_identity line 936

Source documentation

Exact error identity for the bilinear full physical DN pairing.

theorem DN_quasimode_identity (ha : Admissible Ω lam mu) (hO : IsOpen Ω)
    (hB : Bornology.IsBounded Ω) (u v : H1Hilbert Ω) :
    energy Ω lam mu (h1Equiv Ω u) (h1Equiv Ω v) -
      DN Ω lam mu (trace Ω (h1Equiv Ω u)) (trace Ω (h1Equiv Ω v)) =
      zeroTraceEnergy (ha.1.boundedCoefficient hO hB) (ha.2.1.boundedCoefficient hO hB)
        (physicalError ha hO hB u) (physicalError ha hO hB v) := by
…

Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.H1Hilbert, OAI.Elasticity.energy, OAI.Elasticity.h1Equiv, OAI.Elasticity.DN, OAI.Elasticity.trace, OAI.Elasticity.zeroTraceEnergy, OAI.Elasticity.physicalError

theorem OAI.Elasticity.DN_quasimode_bound line 966

Source documentation

The DN error is quadratic in the dual residual, uniformly over all trials. This bound loses no derivative and uses no pointwise boundary assumptions.

theorem DN_quasimode_bound (ha : Admissible Ω lam mu) (hO : IsOpen Ω)
    (hB : Bornology.IsBounded Ω) :
    ∃ C : ℝ, 0 < C ∧ ∀ u v : H1Hilbert Ω,
      |energy Ω lam mu (h1Equiv Ω u) (h1Equiv Ω v) -
        DN Ω lam mu (trace Ω (h1Equiv Ω u)) (trace Ω (h1Equiv Ω v))| ≤
      C * ‖physicalResidual (ha.1.boundedCoefficient hO hB)
        (ha.2.1.boundedCoefficient hO hB) u‖ *
        ‖physicalResidual (ha.1.boundedCoefficient hO hB)
        (ha.2.1.boundedCoefficient hO hB) v‖ := by
…

Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.H1Hilbert, OAI.Elasticity.energy, OAI.Elasticity.h1Equiv, OAI.Elasticity.DN, OAI.Elasticity.trace, OAI.Elasticity.physicalResidual

theorem OAI.Elasticity.equal_DN_quasimode_bound line 993

Source documentation

An exact quantitative comparison for two actual equal physical DN maps. The trials may differ, provided their traces agree; the errors are calculated separately in the two genuine physical systems.

theorem equal_DN_quasimode_bound {l₁ m₁ l₂ m₂ : X → ℝ}
    (ha₁ : Admissible Ω l₁ m₁) (ha₂ : Admissible Ω l₂ m₂)
    (hO : IsOpen Ω) (hB : Bornology.IsBounded Ω)
    (hDN : DN Ω l₁ m₁ = DN Ω l₂ m₂) :
    ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ 0 < C₂ ∧
      ∀ u₁ v₁ u₂ v₂ : H1Hilbert Ω,
      trace Ω (h1Equiv Ω u₁) = trace Ω (h1Equiv Ω u₂) →
      trace Ω (h1Equiv Ω v₁) = trace Ω (h1Equiv Ω v₂) →
      |energy Ω l₁ m₁ (h1Equiv Ω u₁) (h1Equiv Ω v₁) -
        energy Ω l₂ m₂ (h1Equiv Ω u₂) (h1Equiv Ω v₂)| ≤
      C₁ * ‖physicalResidual (ha₁.1.boundedCoefficient hO hB)
        (ha₁.2.1.boundedCoefficient hO hB) u₁‖ *
…

Mentions: OAI.Elasticity.X, OAI.Elasticity.Admissible, OAI.Elasticity.DN, OAI.Elasticity.H1Hilbert, OAI.Elasticity.trace, OAI.Elasticity.h1Equiv, OAI.Elasticity.energy, OAI.Elasticity.physicalResidual