OAI/MathematicalPhysics/Elasticity/Transfer.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElasticityCGO.S line 14
2. def OAI.ElasticityCGO.cut line 18

   Source documentation

   A compact cutoff acts on every smooth amplitude, without any temperate assumption on the amplitude itself.

   def cut (χ : Smooth) (hc : HasCompactSupport (χ : X → ℂ)) : Smooth →ₗ[ℂ] S where
   …

   Mentions: OAI.ElasticityCGO.S

3. lemma OAI.ElasticityCGO.cut_apply line 29
4. lemma OAI.ElasticityCGO.cut_local line 31
5. lemma OAI.ElasticityCGO.physical_cut_local line 37
6. def OAI.ElasticityCGO.residual0 line 51
7. def OAI.ElasticityCGO.residual1 line 54
8. theorem OAI.ElasticityCGO.cut_truncation_residual line 59

   Source documentation

   The actual Schwartz residual has precisely the two powers h^8 and h^7. The amplitude recursions are only required on the indicated open region.

   theorem cut_truncation_residual {U : Set X} (hU : IsOpen U)
       (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (lam m χ : Smooth)
       (hl : (lam : X → ℂ).HasTemperateGrowth) (hm : (m : X → ℂ).HasTemperateGrowth)
       (hc : HasCompactSupport (χ : X → ℂ)) (hχ : EqOn (χ : X → ℂ) 1 U)
       (h : ℝ) (hh : h≠0) (a : ℕ → Amplitude Smooth)
       (hR₀ : leadingR (localCoord hU) θ (restrictSmooth U lam) (restrictSmooth U m)
         (localAmp U (a 0)).1 (localAmp U (a 0)).2=0)
       (hn₀ : normal θ (a 0).1=0)
       (hrec : ∀ j<8,RecursOn hU θ lam m (a j) (a (j+1))) (i : Fin 3) :
       EqOn (physical ((h : ℂ)⁻¹ • θ) lam m
         (fun j => cut χ hc ((truncation (h : ℂ) 8 a).1 j)) i : X → ℂ)
         (finiteResidual h (fun j => cut χ hc (residual0 lam m (a 8) j))
   …

   Mentions: OAI.ElasticityCGO.cut, OAI.ElasticityCGO.residual0

9. lemma OAI.ElasticityCGO.phase_eq line 85
10. lemma OAI.ElasticityPhysicalAlgebra.physical_eqOn_of_eqOn line 100
11. theorem OAI.ElasticityPhysicalAlgebra.compactify_physical_transfer line 117

    Source documentation

    A local physical transfer that agrees off a compact set gives a genuinely compact supported global difference, without changing the physical equation on its open domain.

    theorem compactify_physical_transfer {K U : Set X} (hK : IsCompact K)
        (hU : IsOpen U) (hKU : K⊆U) (lam m : Smooth)
        (hl : (lam : X → ℂ).HasTemperateGrowth) (hm : (m : X → ℂ).HasTemperateGrowth)
        (F G : Fin 3 → SchwartzMap X ℂ) (hG : ∀ i,EqOn (physical 0 lam m G i : X → ℂ) 0 U)
        (he : ∀ i,EqOn (G i : X → ℂ) (F i) (U\K)) :
        ∃ H : Fin 3 → SchwartzMap X ℂ,(∀ i,tsupport (H i)⊆K) ∧
          (∀ i,EqOn (physical 0 lam m (F+H) i : X → ℂ) 0 U) ∧
          (∀ i,EqOn ((F+H) i : X → ℂ) (G i) U) := by
    …

    Mentions: OAI.ElasticityPhysicalAlgebra.X, OAI.ElasticityPhysicalAlgebra.Smooth, OAI.ElasticityPhysicalAlgebra.physical

12. theorem OAI.Elasticity.physical_supported_transfer line 161

    Source documentation

    A supported smooth physical difference derived from the actual DN equality. This is the literal compact support needed for the augmented Carleman estimate.

    theorem physical_supported_transfer
        (ha₁ : Admissible Ω lam₁ mu₁) (ha₂ : Admissible Ω lam₂ mu₂)
        (hΩ : IsOpen Ω) (hOB : Bornology.IsBounded Ω) (hΩB : Ω⊆B)
        (hB : IsOpen B) (hB' : IsOpen B') (hsub : B'⊆B) (hcl : closure Ω⊆B')
        (hl₁ : BoundedCoefficient B lam₁) (hm₁ : BoundedCoefficient B mu₁)
        (hl₂ : BoundedCoefficient B lam₂) (hm₂ : BoundedCoefficient B mu₂)
        (he : ∀ x∉Ω, lam₁ x=lam₂ x ∧ mu₁ x=mu₂ x)
        (hDN : DN Ω lam₁ mu₁=DN Ω lam₂ mu₂)
        (L₁ M₁ L₂ M₂ N₂ O₂ : Coeff) (hN : N₂*M₂=1) (hO : O₂*(L₂+M₂+M₂)=1)
        (hL₁ : ∀ᵐ x ∂(volume.restrict B), eval L₁ x=(lam₁ x : ℂ))
        (hM₁ : ∀ᵐ x ∂(volume.restrict B), eval M₁ x=(mu₁ x : ℂ))
        (hL₂ : ∀ᵐ x ∂(volume.restrict B), eval L₂ x=(lam₂ x : ℂ))
    …

    Mentions: OAI.Elasticity.Admissible, OAI.Elasticity.BoundedCoefficient, OAI.Elasticity.DN

13. lemma OAI.ElasticityAugmented.deriv_phase_mul line 202
14. theorem OAI.ElasticityAugmented.physical_phase_conjugation line 210

    Source documentation

    The shifted operator is the literal exponential conjugation of the physical stress-divergence, not a new PDE declared equivalent by hypothesis.

    theorem physical_phase_conjugation (hχ : ∀ i,D i χ=z i • χ)
        (lam m : A) (u : ι → A) (i : ι) :
        LT (fun j => (D j).toLinearMap) lam m (fun j => χ*u j) i =
          χ*LT (shifted D z) lam m u i := by
    …

    Mentions: OAI.ElasticityAugmented.LT, OAI.ElasticityAugmented.shifted

15. def OAI.ElasticityAugmented.exponential line 229

    Source documentation

    An arbitrary complex linear frequency gives a genuine global smooth exponential on the physical real space.

    def exponential (L : X →L[ℝ] ℂ) : Smooth := ⟨fun x => Complex.exp (L x),by
    …

    Mentions: OAI.ElasticityAugmented.X, OAI.ElasticityAugmented.Smooth

16. lemma OAI.ElasticityAugmented.coord_exponential line 231
17. lemma OAI.ElasticityAugmented.exponential_ne_zero line 238
18. theorem OAI.ElasticityAugmented.physical_exponential_conjugation line 241
19. abbrev OAI.ElasticityCarleman.X line 257
20. abbrev OAI.ElasticityCarleman.Y line 258
21. abbrev OAI.ElasticityCarleman.Direction line 259
22. def OAI.ElasticityCarleman.e line 261
23. def OAI.ElasticityCarleman.deriv line 263
24. def OAI.ElasticityCarleman.laplacian line 266
25. def OAI.ElasticityCarleman.phase line 269
26. def OAI.ElasticityCarleman.conjugate line 271
27. def OAI.ElasticityCarleman.sobolevNorm line 276

    Source documentation

    The sum-of-component semiclassical Fourier norm, written using the Euclidean norm on the target; this is exactly that sum under the square root.

    def sobolevNorm (h s : ℝ) (f : X → Y) : ℝ :=
    …

    Mentions: OAI.ElasticityCarleman.X, OAI.ElasticityCarleman.Y

28. def OAI.ElasticityCarleman.normalizedOperator line 279
29. def OAI.ElasticityCarleman.SupportedCarlemanClaim line 283
30. def OAI.ElasticityCarleman.phaseCLM line 296

    Source documentation

    The real-linear complex phase functional.

    def phaseCLM (θ : Direction) : X →L[ℝ] ℂ :=
    …

    Mentions: OAI.ElasticityCarleman.Direction, OAI.ElasticityCarleman.X

31. lemma OAI.ElasticityCarleman.phaseCLM_apply line 299
32. lemma OAI.ElasticityCarleman.phaseCLM_e line 302
33. def OAI.ElasticityCarleman.expPhase line 305
34. lemma OAI.ElasticityCarleman.contDiff_expPhase line 307
35. lemma OAI.ElasticityCarleman.fderiv_expPhase line 315
36. lemma OAI.ElasticityCarleman.contDiff_deriv line 321
37. lemma OAI.ElasticityCarleman.deriv_add line 325
38. lemma OAI.ElasticityCarleman.deriv_const_smul line 330
39. lemma OAI.ElasticityCarleman.deriv_expPhase_smul line 337
40. lemma OAI.ElasticityCarleman.second_deriv_expPhase_smul line 346
41. lemma OAI.ElasticityCarleman.laplacian_expPhase_smul line 364

    Source documentation

    Exact second-order conjugation before using the characteristic equation.

    lemma laplacian_expPhase_smul {f : X → Y} (hf : ContDiff ℝ (⊤ : ℕ∞) f)
        (θ : Direction) (z : ℂ) :
        laplacian (fun x => expPhase θ z x • f x) = fun x =>
          expPhase θ z x • (laplacian f x +
            (2 * z) • (∑ i, θ i • deriv f i x) +
            (z ^ 2 * (∑ i, θ i * θ i)) • f x) := by
    …

    Mentions: OAI.ElasticityCarleman.X, OAI.ElasticityCarleman.Y, OAI.ElasticityCarleman.Direction, OAI.ElasticityCarleman.laplacian, OAI.ElasticityCarleman.expPhase, OAI.ElasticityCarleman.deriv

42. lemma OAI.ElasticityCarleman.laplacian_expPhase_smul_null line 389

    Source documentation

    The null phase removes the order-two parameter term, exactly as used in both the supported estimate and the formal physical recursion.

    lemma laplacian_expPhase_smul_null {f : X → Y} (hf : ContDiff ℝ (⊤ : ℕ∞) f)
        (θ : Direction) (hθ : (∑ i, θ i * θ i) = 0) (z : ℂ) :
        laplacian (fun x => expPhase θ z x • f x) = fun x =>
          expPhase θ z x • (laplacian f x + (2 * z) • (∑ i, θ i • deriv f i x)) := by
    …

    Mentions: OAI.ElasticityCarleman.X, OAI.ElasticityCarleman.Y, OAI.ElasticityCarleman.Direction, OAI.ElasticityCarleman.laplacian, OAI.ElasticityCarleman.expPhase, OAI.ElasticityCarleman.deriv

43. lemma OAI.ElasticityCarleman.normalized_expPhase_smul line 396

    Source documentation

    Full normalized conjugation identity, retaining the lower-order matrices.

    lemma normalized_expPhase_smul {f : X → Y} (hf : ContDiff ℝ (⊤ : ℕ∞) f)
        (A : Fin 3 → X → Y →L[ℂ] Y) (A₀ : X → Y →L[ℂ] Y)
        (θ : Direction) (hθ : (∑ i, θ i * θ i) = 0) (z : ℂ) :
        normalizedOperator A A₀ (fun x => expPhase θ z x • f x) =
          fun x => expPhase θ z x • (normalizedOperator A A₀ f x +
            (2 * z) • (∑ i, θ i • deriv f i x) +
            z • (∑ i, θ i • A i x (f x))) := by
    …

    Mentions: OAI.ElasticityCarleman.X, OAI.ElasticityCarleman.Y, OAI.ElasticityCarleman.Direction, OAI.ElasticityCarleman.normalizedOperator, OAI.ElasticityCarleman.expPhase, OAI.ElasticityCarleman.deriv

44. def OAI.ElasticityCGO.expCut line 424

    Source documentation

    Actual Schwartz representatives of the exponential physical fields on a bounded region. No temperate behavior of the exponential is assumed.

    def expCut (χ : Smooth) (hc : HasCompactSupport (χ : X → ℂ))
        (z : Fin 3 → ℂ) (f : S) : S :=
    …

    Mentions: OAI.ElasticityCGO.S

45. lemma OAI.ElasticityCGO.expCut_apply line 427
46. lemma OAI.ElasticityCGO.shifted_zero line 432
47. lemma OAI.ElasticityCGO.phaseCLM_coords line 438
48. theorem OAI.ElasticityCGO.expCut_physical line 443

    Source documentation

    The literal unshifted stress-divergence of a cut-off exponential field.

    theorem expCut_physical {U : Set X} (hU : IsOpen U) (lam m χ : Smooth)
        (hl : (lam : X → ℂ).HasTemperateGrowth) (hm : (m : X → ℂ).HasTemperateGrowth)
        (hc : HasCompactSupport (χ : X → ℂ)) (hχ : EqOn (χ : X → ℂ) 1 U)
        (z : Fin 3 → ℂ) (f : Fin 3 → S) (i : Fin 3) :
        EqOn (physical 0 lam m (fun j => expCut χ hc z (f j)) i : X → ℂ)
          (fun x => Complex.exp (phaseCLM z x)*physical z lam m f i x) U := by
    …

    Mentions: OAI.ElasticityCGO.S, OAI.ElasticityCGO.expCut

49. theorem OAI.ElasticityCGO.expCut_solution line 455
50. theorem OAI.ElasticityCGO.div_exponential line 468

    Source documentation

    The full actual divergence is the exponential times the shifted divergence.

    theorem div_exponential (z : Fin 3 → ℂ) (u : Fin 3 → Smooth) :
        div coord (fun j => exponential (phaseCLM z)*u j)=
          exponential (phaseCLM z)*divT (shifted coord z) u := by
    …

51. lemma OAI.ElasticityCGO.phaseCLM_neg line 488
52. lemma OAI.ElasticityCGO.expCut_support line 493
53. theorem OAI.ElasticityCGO.transferred_amplitude line 505

    Source documentation

    Factoring the transferred PHYSICAL solution gives a shifted physical solution. The compact difference is multiplied by the inverse exponential only on a compact support, never regarded as a global temperate multiplier.

    theorem transferred_amplitude {B K : Set X} (hB : IsOpen B)
        (lam m χ : Smooth) (hl : (lam : X → ℂ).HasTemperateGrowth)
        (hm : (m : X → ℂ).HasTemperateGrowth) (hc : HasCompactSupport (χ : X → ℂ))
        (hχ : EqOn (χ : X → ℂ) 1 B) (z : Fin 3 → ℂ) (u F H : Fin 3 → S)
        (hF : ∀ i x,x∈B → F i x=Complex.exp (phaseCLM z x)*u i x)
        (hH : ∀ i,tsupport (H i : X → ℂ)⊆K)
        (hsol : ∀ i,EqOn (physical 0 lam m (F+H) i : X → ℂ) 0 B) :
        ∃ v : Fin 3 → S,
          (∀ i,tsupport (v i-u i : S)⊆K) ∧
          (∀ i,EqOn (physical z lam m v i : X → ℂ) 0 B) ∧
          (∀ i x,x∈B → Complex.exp (phaseCLM z x)*v i x=F i x+H i x) := by
    …

    Mentions: OAI.ElasticityCGO.S

54. lemma OAI.ElasticityCGO.divShift_supported line 541

    Source documentation

    The actual shifted divergence of the compact physical difference also has compact support; no separate scalar field is introduced.

    lemma divShift_supported {K : Set X} (hK : IsClosed K) (z : Fin 3 → ℂ)
        (u : Fin 3 → S) (hu : ∀ i,tsupport (u i : X → ℂ)⊆K) :
        tsupport (divShift z u : X → ℂ)⊆K := by
    …

    Mentions: OAI.ElasticityCGO.S

55. def OAI.ElasticityPhysicalEstimate.physicalAug line 571

    Source documentation

    The scalar component is the actual shifted divergence.

    def physicalAug (z : Fin 3 → ℂ) (u : Fin 3 → S) : Fin 4 → S :=
    …

56. lemma OAI.ElasticityPhysicalEstimate.physicalAug_sub line 574
57. lemma OAI.ElasticityPhysicalEstimate.physicalAug_supported line 581
58. theorem OAI.ElasticityPhysicalEstimate.physical_compact_comparison line 588
59. lemma OAI.Elasticity.energy_coeff_congr_ae line 668
60. theorem OAI.Elasticity.DN_coeff_congr_ae line 678

    Source documentation

    The variational DN definition really depends only on the interior coefficients, including its choice branch. No exterior identification is presumed.

    theorem DN_coeff_congr_ae
        (hl : l₁ =ᵐ[volume.restrict Ω] l₂) (hm : m₁ =ᵐ[volume.restrict Ω] m₂) :
        DN Ω l₁ m₁=DN Ω l₂ m₂ := by
    …

    Mentions: OAI.Elasticity.DN

61. theorem OAI.Elasticity.DN_coeff_congr line 695