OAI/MathematicalPhysics/Elasticity/Carleman.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElasticityPhysicalEstimate.X line 12
2. lemma OAI.ElasticityPhysicalEstimate.J_sum line 14
3. lemma OAI.ElasticityPhysicalEstimate.negNorm_sum_le line 18
4. lemma OAI.ElasticityPhysicalEstimate.sumNorm_three_le line 23
5. lemma OAI.ElasticityPhysicalEstimate.dirDeriv_negNorm line 33
6. def OAI.ElasticityPhysicalEstimate.augmentedForcing line 57

   Source documentation

   The actual normalized forcing generated by a physical forcing F. Here n=1/μ, o=1/(λ+2μ), and c_i=-2(∂ᵢμ)/μ. The scalar entry contains the conjugated divergence.

   def augmentedForcing (h : ℝ) (α β : X) (n o : X → ℂ) (c : Fin 3 → X → ℂ)
       (F : Fin 3 → S) : Fin 4 → S :=
   …

   Mentions: OAI.ElasticityPhysicalEstimate.X

7. lemma OAI.ElasticityPhysicalEstimate.forcing_bound line 62
8. lemma OAI.ElasticityPhysicalEstimate.dirDeriv_norm line 133
9. lemma OAI.ElasticityPhysicalEstimate.lowerDir_norm line 153
10. lemma OAI.ElasticityPhysicalEstimate.system_difference_bound line 187
11. theorem OAI.ElasticityPhysicalEstimate.compact_comparison_estimate line 234

    Source documentation

    The exact compact comparison estimate: the common second-order principal part cancels, and the h factor in its actual lower-order forcing cancels the Carleman 1/h loss. This dependency does not assert that the physical DN transfer has already supplied the forcing identity.

    theorem compact_comparison_estimate (R : ℝ) (hR : 1≤R) (α β : X) (hα : α≠0)
        (a b : Fin 3 → Fin 4 → Fin 4 → X → ℂ) (v w : Fin 4 → Fin 4 → X → ℂ)
        (ha : ∀ k i j,(a k i j).HasTemperateGrowth) (hb : ∀ k i j,(b k i j).HasTemperateGrowth)
        (hv : ∀ i j,(v i j).HasTemperateGrowth) (hw : ∀ i j,(w i j).HasTemperateGrowth)
        (A V Z : ℝ) (hA : 0≤A) (hV : 0≤V) (hZ : 0≤Z)
        (haA : ∀ k i j x,‖a k i j x‖≤A) (hbA : ∀ k i j x,‖b k i j x‖≤A)
        (hvV : ∀ i j x,‖v i j x‖≤V) (hwV : ∀ i j x,‖w i j x‖≤V)
        (hz : ∀ i,‖((α i : ℂ)+Complex.I*(β i : ℂ))‖≤Z) :
        ∃ C h₀ : ℝ,0<C ∧ 0<h₀ ∧ ∀ h : ℝ,0<h → h≤h₀ →
          ∀ U W : Fin 4 → S,(∀ i,BallSupported R (W i)) →
          dirSystem h α β b w W=dirSystem h α β a v U-dirSystem h α β b w U →
          sobNorm h 1 W≤C*sobNorm h 1 U := by
    …

    Mentions: OAI.ElasticityPhysicalEstimate.X

12. abbrev OAI.ElasticityPhysicalAlgebra.X line 266
13. abbrev OAI.ElasticityPhysicalAlgebra.Smooth line 267
14. lemma OAI.ElasticityPhysicalAlgebra.temperate_fderiv line 269
15. lemma OAI.ElasticityPhysicalAlgebra.temperate_partial line 276
16. def OAI.ElasticityPhysicalAlgebra.toSmooth line 281

    Source documentation

    The genuine embedding of Schwartz functions into the smooth differential algebra.

    def toSmooth : S →ₗ[ℂ] Smooth where
    …

    Mentions: OAI.ElasticityPhysicalAlgebra.Smooth

17. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_apply line 286
18. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_injective line 288
19. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_d line 293
20. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_mult line 298
21. def OAI.ElasticityPhysicalAlgebra.shiftD line 305

    Source documentation

    Constant complex phase shift, still an actual differential operator on Schwartz maps.

    def shiftD (z : Fin 3 → ℂ) (i : Fin 3) : S →ₗ[ℂ] S := d (e i) + z i • LinearMap.id

22. lemma OAI.ElasticityPhysicalAlgebra.shiftD_apply line 307
23. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_shiftD line 310
24. def OAI.ElasticityPhysicalAlgebra.physical line 315

    Source documentation

    The conjugated physical stress-divergence, without treating its shifted derivatives as derivations.

    def physical (z : Fin 3 → ℂ) (lam m : X → ℂ) (u : Fin 3 → S) (i : Fin 3) : S :=
    …

    Mentions: OAI.ElasticityPhysicalAlgebra.X

25. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_physical line 319
26. def OAI.ElasticityPhysicalAlgebra.phase line 329
27. lemma OAI.ElasticityPhysicalAlgebra.dirDeriv_eq_shiftD line 332
28. def OAI.ElasticityPhysicalAlgebra.lapShift line 342
29. def OAI.ElasticityPhysicalAlgebra.divShift line 344
30. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_lapShift line 346
31. lemma OAI.ElasticityPhysicalAlgebra.toSmooth_divShift line 351
32. lemma OAI.ElasticityPhysicalAlgebra.Pdir_eq_lapShift line 356
33. lemma OAI.ElasticityPhysicalAlgebra.shiftD_supported line 371
34. lemma OAI.ElasticityPhysicalAlgebra.divShift_supported line 375
35. def OAI.ElasticityAugmented.coeffA line 386
36. def OAI.ElasticityAugmented.coeffV line 393
37. def OAI.ElasticityAugmented.normalizedPair line 398
38. lemma OAI.ElasticityAugmented.normalizedPair_matrix line 402
39. def OAI.ElasticityPhysicalEstimate.aPhys line 433

    Source documentation

    The actual normalized matrix coefficients, with the sign of the Carleman operator.

    def aPhys (lam m n o : Smooth) (k : Fin 3) (i j : Fin 4) : X → ℂ :=
    …

    Mentions: OAI.ElasticityPhysicalEstimate.X

40. def OAI.ElasticityPhysicalEstimate.vPhys line 435
41. def OAI.ElasticityPhysicalEstimate.cPhys line 437
42. lemma OAI.ElasticityPhysicalEstimate.aPhys_growth line 439
43. lemma OAI.ElasticityPhysicalEstimate.vPhys_growth line 443
44. lemma OAI.ElasticityPhysicalEstimate.toSmooth_aPhys line 448
45. lemma OAI.ElasticityPhysicalEstimate.toSmooth_vPhys line 453
46. lemma OAI.ElasticityPhysicalEstimate.toSmooth_dirSystem line 459
47. lemma OAI.ElasticityPhysicalEstimate.toSmooth_forcing line 476
48. lemma OAI.ElasticityPhysicalEstimate.physical_system_identity line 495
49. lemma OAI.ElasticityPhysicalEstimate.norm_tail_le line 520
50. theorem OAI.ElasticityPhysicalEstimate.physical_test_estimate line 532

    Source documentation

    The physical adjoint-test estimate obtained from the actual scalar-principal augmented operator. All coefficients and forcing terms are explicit.

    theorem physical_test_estimate (R : ℝ) (hR : 1 ≤ R) (α β : X) (hα : α ≠ 0)
        (lam m n o : Smooth) (hinv : n*m=1) (hoinv : o*(lam+m+m)=1)
        (hl : (lam : X → ℂ).HasTemperateGrowth) (hm : (m : X → ℂ).HasTemperateGrowth)
        (hn : (n : X → ℂ).HasTemperateGrowth) (ho : (o : X → ℂ).HasTemperateGrowth)
        (ha : ∀ k i j, ((coeffA coord lam m n o k i j : Smooth) : X → ℂ).HasTemperateGrowth)
        (hv : ∀ i j, ((coeffV coord lam m n o i j : Smooth) : X → ℂ).HasTemperateGrowth)
        (hc : ∀ i, (cPhys m n i).HasTemperateGrowth)
        (M V A D Z : ℝ) (hM : 0 ≤ M) (hV : 0 ≤ V) (hA : 0 ≤ A) (hD : 0 ≤ D) (hZ : 0 ≤ Z)
        (haM : ∀ k i j x, ‖aPhys lam m n o k i j x‖ ≤ M)
        (hvV : ∀ i j x, ‖vPhys lam m n o i j x‖ ≤ V)
        (hnA : ∀ x, ‖(n : X → ℂ) x‖ ≤ A) (hoA : ∀ x, ‖(o : X → ℂ) x‖ ≤ A)
        (hcA : ∀ i x, ‖cPhys m n i x‖ ≤ A)
    …

    Mentions: OAI.ElasticityPhysicalEstimate.X, OAI.ElasticityPhysicalEstimate.cPhys, OAI.ElasticityPhysicalEstimate.aPhys, OAI.ElasticityPhysicalEstimate.vPhys

51. lemma OAI.ElasticityPhysicalEstimate.deriv_zero_on line 587
52. lemma OAI.ElasticityPhysicalEstimate.dirDeriv_zero_on line 597
53. theorem OAI.ElasticityPhysicalEstimate.physical_dirSystem_on line 606

    Source documentation

    A local physical solution satisfies the actual normalized four-system, including its scalar row, on the same open set.

    theorem physical_dirSystem_on {B : Set X} (hB : IsOpen B)
        (h : ℝ) (hh : h≠0) (α β : X)
        (lam m n o : Smooth) (hinv : n*m=1) (hoinv : o*(lam+m+m)=1)
        (hl : (lam : X → ℂ).HasTemperateGrowth) (hm : (m : X → ℂ).HasTemperateGrowth)
        (hn : (n : X → ℂ).HasTemperateGrowth) (ho : (o : X → ℂ).HasTemperateGrowth)
        (ha : ∀ k i j,((coeffA coord lam m n o k i j : Smooth) : X → ℂ).HasTemperateGrowth)
        (hv : ∀ i j,((coeffV coord lam m n o i j : Smooth) : X → ℂ).HasTemperateGrowth)
        (hc : ∀ i,(cPhys m n i).HasTemperateGrowth)
        (u : Fin 3 → S) (hu : ∀ i,EqOn (physical (phase h α β) lam m u i : X → ℂ) 0 B) :
        ∀ i,EqOn (dirSystem h α β (aPhys lam m n o) (vPhys lam m n o)
          (Fin.cons (divShift (phase h α β) u) u) i : X → ℂ) 0 B := by
    …

    Mentions: OAI.ElasticityPhysicalEstimate.X, OAI.ElasticityPhysicalEstimate.cPhys, OAI.ElasticityPhysicalEstimate.aPhys, OAI.ElasticityPhysicalEstimate.vPhys

54. lemma OAI.ElasticityPhysicalEstimate.dirSystem_sub line 627
55. lemma OAI.ElasticityPhysicalEstimate.deriv_supported line 645
56. lemma OAI.ElasticityPhysicalEstimate.dirSystem_zero_outside line 649
57. lemma OAI.ElasticityPhysicalEstimate.dirSystem_difference_zero_outside line 663
58. theorem OAI.ElasticityPhysicalEstimate.compact_forcing_identity line 679

    Source documentation

    A genuine local pair of homogeneous normalized solutions with compact supported difference has the global compact forcing identity used by Carleman. Only equality of the lower-order coefficients off K is required; no artificial second-order difference term is introduced.

    theorem compact_forcing_identity {B K : Set X} (hKB : K⊆B) (h : ℝ) (α β : X)
        (a b : Fin 3 → Fin 4 → Fin 4 → X → ℂ) (v w : Fin 4 → Fin 4 → X → ℂ)
        (ha : ∀ k i j,(a k i j).HasTemperateGrowth) (hb : ∀ k i j,(b k i j).HasTemperateGrowth)
        (hv : ∀ i j,(v i j).HasTemperateGrowth) (hw : ∀ i j,(w i j).HasTemperateGrowth)
        (hea : ∀ k i j x,x∉K → a k i j x=b k i j x)
        (hev : ∀ i j x,x∉K → v i j x=w i j x)
        (U V : Fin 4 → S) (hs : ∀ i,tsupport ((V-U) i : X → ℂ)⊆K)
        (hU : ∀ i,EqOn (dirSystem h α β a v U i : X → ℂ) 0 B)
        (hV : ∀ i,EqOn (dirSystem h α β b w V i : X → ℂ) 0 B) :
        dirSystem h α β b w (V-U)=dirSystem h α β a v U-dirSystem h α β b w U := by
    …

    Mentions: OAI.ElasticityPhysicalEstimate.X