BoundaryData.lean`

86 declarations, 0 contain sorry, 0 declared as axioms

Mixed physical quasimodes. Unlike a quadratic same-system remainder, this controls the coefficient-difference energy of a trial for each system. It is the precise physical-DN bridge for the normal-jet induction.

lemma OAI.Elasticity.DN_trace_symm line 17
lemma OAI.Elasticity.DN_one_sided_error line 33
lemma OAI.Elasticity.mixed_error_identity line 49

theorem OAI.Elasticity.equal_DN_mixed_quasimode_bound line 69

Source documentation

Equal physical DN maps control the same mixed fields in the two coefficient energies, using only the residual in its own system.

theorem equal_DN_mixed_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 : H1Hilbert Ω,
      |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‖ * ‖v‖ +
      C₂ * ‖u‖ * ‖physicalResidual (ha₂.1.boundedCoefficient hO hB)
        (ha₂.2.1.boundedCoefficient hO hB) v‖ := by
…

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

abbrev OAI.Elasticity.ComplexTrial line 117
def OAI.Elasticity.complexTrialSize line 119
def OAI.Elasticity.complexTrialEnergy line 121
def OAI.Elasticity.complexResidualSize line 127
lemma OAI.Elasticity.norm_complex_four line 131

theorem OAI.Elasticity.equal_DN_complex_mixed_bound line 142

Source documentation

Genuine sesquilinear mixed energy from equality of the real physical DN maps. Each of the four trial components may have its own arbitrary trace.

theorem equal_DN_complex_mixed_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 : ComplexTrial Ω,
      ‖complexTrialEnergy l₁ m₁ u v-complexTrialEnergy l₂ m₂ u v‖≤
      C₁*complexResidualSize (ha₁.1.boundedCoefficient hO hB)
        (ha₁.2.1.boundedCoefficient hO hB) u*complexTrialSize v+
      C₂*complexTrialSize u*complexResidualSize (ha₂.1.boundedCoefficient hO hB)
        (ha₂.2.1.boundedCoefficient hO hB) v := by
…

Mentions: OAI.Elasticity.X, OAI.Elasticity.Admissible, OAI.Elasticity.DN, OAI.Elasticity.ComplexTrial, OAI.Elasticity.complexTrialEnergy, OAI.Elasticity.complexResidualSize, OAI.Elasticity.complexTrialSize

def OAI.Elasticity.jetStress line 179
lemma OAI.Elasticity.jetStrain_symm line 183
lemma OAI.Elasticity.jetEnergy_stress line 187

lemma OAI.Elasticity.boundary_smooth_ibp line 214

Source documentation

Smooth scalar integration by parts with a compactly supported interior test.

lemma boundary_smooth_ibp {f : X → ℝ} (hf : ContDiff ℝ (⊤ : ℕ∞) f)
    (g : SchwartzMap X ℝ) (hc : HasCompactSupport (g : X → ℝ))
    (hs : tsupport (g : X → ℝ) ⊆ Ω) (j : Fin 3) :
    (∫ x, f x*ElasticityKorn.d (coordVector j) g x ∂(volume.restrict Ω)) =
    -(∫ x, fderiv ℝ f x (coordVector j)*g x ∂(volume.restrict Ω)) := by
…

Mentions: OAI.Elasticity.X, OAI.ElasticityKorn.d, OAI.Elasticity.coordVector

lemma OAI.Elasticity.boundary_L2_schwartz_pair line 236
def OAI.Elasticity.boundaryForcePair line 246
Source documentation
The actual L2 force pairing, with no regularity required of the test.
```
def boundaryForcePair (F : Fin 3 → ScalarL2 Ω) : JetH Ω →L[ℝ] ℝ :=
…
```
Mentions: OAI.Elasticity.ScalarL2, OAI.Elasticity.JetH
lemma OAI.Elasticity.boundaryForcePair_apply line 249

theorem OAI.Elasticity.physicalResidual_of_smooth_stress line 256

Source documentation

Smooth stresses with their literal divergence give exactly the physical variational residual. The same statement permits local coefficient extensions: only equality to the actual stress on Ω is required.

theorem physicalResidual_of_smooth_stress
    (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
    (hB : Bornology.IsBounded Ω) (u : H1Hilbert Ω) (s : Fin 3 → Fin 3 → X → ℝ)
    (hs : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (s i j))
    (hes : ∀ i j, jetStress hl hm u.val i j =ᵐ[volume.restrict Ω] s i j)
    (hd : ∀ i j, MemLp (fun x => fderiv ℝ (s i j) x (coordVector j)) 2 (volume.restrict Ω)) :
    physicalResidual hl hm u =
      -(boundaryForcePair (fun i => ∑ j, (hd i j).toLp _)).comp (H10Hilbert Ω).subtypeL := by
…

Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1Hilbert, OAI.Elasticity.X, OAI.Elasticity.jetStress, OAI.Elasticity.coordVector, OAI.Elasticity.physicalResidual, OAI.Elasticity.boundaryForcePair, OAI.Elasticity.H10Hilbert

lemma OAI.Elasticity.jetScalar_value_norm_le line 296
lemma OAI.Elasticity.boundaryForcePair_norm_le line 308

theorem OAI.Elasticity.physicalResidual_norm_le_of_smooth_stress line 325

Source documentation

The actual dual residual obeys an L2 strong-residual bound; no boundary regularity of the test space or unproved trace density is used.

theorem physicalResidual_norm_le_of_smooth_stress
    (hl : BoundedCoefficient Ω lam) (hm : BoundedCoefficient Ω mu)
    (hB : Bornology.IsBounded Ω) (u : H1Hilbert Ω) (s : Fin 3 → Fin 3 → X → ℝ)
    (hs : ∀ i j, ContDiff ℝ (⊤ : ℕ∞) (s i j))
    (hes : ∀ i j, jetStress hl hm u.val i j =ᵐ[volume.restrict Ω] s i j)
    (hd : ∀ i j, MemLp (fun x => fderiv ℝ (s i j) x (coordVector j)) 2 (volume.restrict Ω)) :
    ‖physicalResidual hl hm u‖ ≤ ∑ i, ‖∑ j, (hd i j).toLp _‖ := by
…

Mentions: OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.H1Hilbert, OAI.Elasticity.X, OAI.Elasticity.jetStress, OAI.Elasticity.coordVector, OAI.Elasticity.physicalResidual

def OAI.Elasticity.smoothTrial line 348
lemma OAI.Elasticity.smoothTrial_value line 354
lemma OAI.Elasticity.smoothTrial_deriv line 359
lemma OAI.Elasticity.smoothTrial_entry_ae line 364
lemma OAI.Elasticity.smoothTrial_stress_ae line 372
lemma OAI.Elasticity.smooth_compact_coordDeriv line 405
lemma OAI.Elasticity.smooth_compact_memLp line 410
lemma OAI.Elasticity.smoothTrial_gradient_ae line 425
lemma OAI.Elasticity.smoothTrial_energy line 434
def OAI.Elasticity.realField line 448
Source documentation
Projection of a complex physical displacement to an actual real trial field. The map w will be real or imaginary part.
```
def realField (w : ℂ →L[ℝ] ℝ) (u : Fin 3 → X → ℂ) (x : X) : V :=
…
```
Mentions: OAI.Elasticity.X, OAI.Elasticity.V
lemma OAI.Elasticity.smooth_realField line 451
lemma OAI.Elasticity.realField_derivative line 455
lemma OAI.Elasticity.realField_support line 467
lemma OAI.Elasticity.compact_realField line 476
abbrev OAI.ElasticityBoundaryProjectedStress.I line 488
abbrev OAI.ElasticityBoundaryProjectedStress.X line 489
def OAI.ElasticityBoundaryProjectedStress.realStress line 491
lemma OAI.ElasticityBoundaryProjectedStress.smooth_stress line 494
lemma OAI.ElasticityBoundaryProjectedStress.compact_stress line 508
lemma OAI.ElasticityBoundaryProjectedStress.project_mul line 527
lemma OAI.ElasticityBoundaryProjectedStress.realStress_eq line 530
lemma OAI.ElasticityBoundaryProjectedStress.smooth_realStress line 540
lemma OAI.ElasticityBoundaryProjectedStress.compact_realStress line 547
lemma OAI.ElasticityBoundaryProjectedStress.derivative_project line 552
lemma OAI.ElasticityBoundaryProjectedStress.realStress_divergence line 559
lemma OAI.Elasticity.L2_norm_sq_mass line 582
lemma OAI.Elasticity.sum_toLp_norm_sq line 586
lemma OAI.Elasticity.sum_three_sq line 594
lemma OAI.Elasticity.physicalResidual_sq_mass line 598
abbrev OAI.ElasticityBoundaryResidualMass.I line 616
abbrev OAI.ElasticityBoundaryResidualMass.X line 617
lemma OAI.ElasticityBoundaryResidualMass.projected_force_mass_le line 619

theorem OAI.ElasticityBoundaryResidualMass.projected_trial_residual line 632

Source documentation

Each real projection is an actual finite-energy smooth trial and its physical variational residual is controlled by the literal complex force.

theorem projected_trial_residual {Ω : Set X} (w : ℂ →L[ℝ] ℝ) {l m : X → ℝ}
    (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (hbl : BoundedCoefficient Ω l) (hbm : BoundedCoefficient Ω m)
    (hB : Bornology.IsBounded Ω)
    (u : I → X → ℂ) (hu : ∀ j, ContDiff ℝ (⊤ : ℕ∞) (u j))
    (hcu : ∀ j, HasCompactSupport (u j))
    (hf : MemLp (realField w u) 2 (volume.restrict Ω))
    (hdf : ∀ j, MemLp (coordDeriv (realField w u) j) 2 (volume.restrict Ω))
    (hF : ∀ i, MemLp (force (fun z => (l z:ℂ)) (fun z => (m z:ℂ)) u i) 2 (volume.restrict Ω)) :
    ‖physicalResidual hbl hbm (smoothTrial (realField w u) (smooth_realField w u hu) hf hdf)‖^2≤
      3*‖w‖^2*∑ i, (∫ x in Ω, ‖force (fun z => (l z:ℂ)) (fun z => (m z:ℂ)) u i x‖^2) := by
…

Mentions: OAI.ElasticityBoundaryResidualMass.X, OAI.ElasticityBoundaryResidualMass.I

lemma OAI.Elasticity.vector_toLp_norm_sq line 673
lemma OAI.Elasticity.smoothTrial_norm_sq line 684
abbrev OAI.ElasticityBoundaryTrialMass.I line 696
abbrev OAI.ElasticityBoundaryTrialMass.X line 697
lemma OAI.ElasticityBoundaryTrialMass.projected_trial_mass line 699
lemma OAI.Elasticity.classicalDensity_integrable line 730
def OAI.Elasticity.projectedTrial line 753
def OAI.Elasticity.complexFieldTrial line 760
def OAI.Elasticity.realMatrix line 765
def OAI.Elasticity.complexDensity line 768
def OAI.Elasticity.fieldGradient line 774
lemma OAI.Elasticity.realMatrix_gradient line 777
lemma OAI.Elasticity.complexFieldTrial_energy line 784
def OAI.ElasticityBoundaryPacket.Setup.field line 827
lemma OAI.ElasticityBoundaryPacket.Setup.cutoff_layer_support line 830
lemma OAI.ElasticityBoundaryPacket.Setup.field_smooth line 837
lemma OAI.ElasticityBoundaryPacket.Setup.field_support line 842
lemma OAI.ElasticityBoundaryPacket.Setup.image_compact line 846
lemma OAI.ElasticityBoundaryPacket.Setup.field_compact line 849
lemma OAI.ElasticityBoundaryPacket.Setup.field_value_mass line 854
lemma OAI.ElasticityBoundaryPacket.Setup.field_gradient_mass line 868

lemma OAI.ElasticityBoundaryPacket.Setup.field_force_mass line 885

Source documentation

Uniform strong force of arbitrary order for the literal physical Lamé operator; its lower terms and the actual curved chart are retained.

lemma Setup.field_force_mass (s : Setup Ω x) (hΩ : MeasurableSet Ω)
    {l m : X → ℂ} (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (hm0 : m x≠0) (he0 : l x+2*m x≠0) (hp0 : l x+3*m x≠0)
    (p₀ : W) (h₀ : normal (l x) (m x) p₀=0) (N : ℕ) :
    ∃ p : ℕ → W, p 0=p₀ ∧ (∀ n, 0<n → boundary (p n)=0) ∧
      ∃ C : ℝ, 0≤C ∧ ∀ δ : ℝ, 0<δ → δ≤1 → ∀ i,
        (∫ z in Ω, ‖force l m (s.field (amplitude p (N+1)) δ) i z‖^2)≤C*δ^(2*N) := by
…

Mentions: OAI.ElasticityBoundaryPacket.Setup, OAI.ElasticityBoundaryPacket.X

lemma OAI.ElasticityBoundaryPacket.smooth_force line 926
lemma OAI.ElasticityBoundaryPacket.compact_force line 935
lemma OAI.ElasticityBoundaryPacket.coarse_sq_bound line 941
def OAI.ElasticityBoundaryPacket.Setup.trial line 950
lemma OAI.ElasticityBoundaryPacket.Setup.trial_size line 953
lemma OAI.ElasticityBoundaryPacket.Setup.trial_residual line 985
lemma OAI.ElasticityBoundaryPacket.amplitude_zero line 1027
lemma OAI.ElasticityBoundaryPacket.ellipticity_at line 1030

lemma OAI.ElasticityBoundaryPacket.Setup.packet line 1040

Source documentation

Genuine physical trace-space test, prescribed leading frozen solution, uniform H1 norm and arbitrarily small dual Lamé residual.

lemma Setup.packet (s : Setup Ω x) {l m : X → ℝ}
    (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (ha : Admissible Ω l m) (hO : IsOpen Ω) (hB : Bornology.IsBounded Ω)
    (hx : x∈closure Ω) (p₀ : W) (h₀ : normal (l x) (m x) p₀=0) (N : ℕ) :
    ∃ q : Polynomial W, q.coeff 0=p₀ ∧ ∃ A B : ℝ, 0≤A ∧ 0≤B ∧
      ∀ δ : ℝ, 0<δ → δ≤1 → complexTrialSize (s.trial q δ)≤A ∧
      complexResidualSize (ha.1.boundedCoefficient hO hB)
        (ha.2.1.boundedCoefficient hO hB) (s.trial q δ)≤B*δ^N := by
…

Mentions: OAI.ElasticityBoundaryPacket.Setup, OAI.ElasticityBoundaryPacket.X

lemma OAI.ElasticityBoundaryPacket.Setup.paired_packets line 1066