OAI/MathematicalPhysics/Elasticity/Smoothing.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Actual Haar/L2 and tempered-distribution change of linear coordinates. The Jacobian is derived from Haar uniqueness, not silently set equal to one.

  1. lemma OAI.ElasticityCoordinates.linear_haar line 19
  2. lemma OAI.ElasticityCoordinates.memLp_linear line 27
  3. def OAI.ElasticityCoordinates.linearPull line 36
  4. lemma OAI.ElasticityCoordinates.linearPull_apply line 42
  5. lemma OAI.ElasticityCoordinates.linearPull_add line 48
  6. lemma OAI.ElasticityCoordinates.linearPull_smul line 54
  7. lemma OAI.ElasticityCoordinates.linearPull_zero line 60
  8. lemma OAI.ElasticityCoordinates.linearPull_deriv line 65
  9. def OAI.ElasticityCoordinates.pullLp line 73
  10. lemma OAI.ElasticityCoordinates.pullLp_coe line 76
  11. lemma OAI.ElasticityCoordinates.pullLp_distribution line 80
  12. lemma OAI.ElasticityCoordinates.pullLp_equation line 101
  13. lemma OAI.ElasticityCoordinates.ae_linear line 124
  14. lemma OAI.ElasticityCoordinates.lp_integrable_supported line 132
  15. theorem OAI.ElasticityCoordinates.planar_smooth_representative line 156

    Source documentation

    Smoothness of an actual compactly supported matrix transport weak solution in arbitrary linear transverse coordinates. The representative equals the original L2 function almost everywhere; no exceptional planes remain.

    theorem planar_smooth_representative (L : (P × ℂ) ≃L[ℝ] E)
    (T K : Set E) (hT : IsCompact T) (hK : IsCompact K)
    (a : n → n → E → ℂ) (ha : ∀ i j,ContDiff ℝ (⊤ : ℕ∞) (a i j))
    (has : ∀ i j x,x∉K → a i j x=0)
    (f : n → E → ℂ) (hf : ∀ i,ContDiff ℝ (⊤ : ℕ∞) (f i))
    (hfs : ∀ i x,x∉K → f i x=0)
    (u w : n → Lp ℂ 2 (volume : Measure E))
    (hus : ∀ i,∀ᵐ x,x∉T → u i x=0) (hws : ∀ i,∀ᵐ x,x∉T → w i x=0)
    (hc : ∀ i,∀ᵐ x,w i x=∑ j,a i j x*u j x-f i x)
    (he : ∀ i,∂_{L (0,1)} (u i : 𝓢'(E,ℂ))+
      Complex.I • ∂_{L (0,Complex.I)} (u i : 𝓢'(E,ℂ))+(w i : 𝓢'(E,ℂ))=0) :
    ∃ v : n → E → ℂ,(∀ i,ContDiff ℝ (⊤ : ℕ∞) (v i)) ∧
…
  16. abbrev OAI.ElasticityDistribution.L2Space line 240
  17. def OAI.ElasticityDistribution.compactLpMul line 242
  18. lemma OAI.ElasticityDistribution.compactLpMul_coe line 245
  19. lemma OAI.ElasticityDistribution.compactLpMul_dist line 252
  20. lemma OAI.ElasticityDistribution.lp_mul_eq line 257
  21. lemma OAI.ElasticityDistribution.lp_mul_zero line 268
  22. lemma OAI.ElasticityDistribution.lp_cutoff_derivative line 283
  23. lemma OAI.ElasticityDistribution.continuous_supported_of_ae line 303
  24. def OAI.ElasticityDistribution.planeDerivative line 327
  25. def OAI.ElasticityDistribution.planeSchwartz line 329
  26. lemma OAI.ElasticityDistribution.planeDerivative_schwartz line 331
  27. theorem OAI.ElasticityDistribution.compact_transport_smoothing line 341

    Source documentation

    Compactly supported differences of the actual weak columns are smooth, including the transverse variable. No inverse of the transferred frame is assumed and no ellipticity in three dimensions is asserted.

    theorem compact_transport_smoothing (L : (P × ℂ) ≃L[ℝ] X)
    {K B B₀ : Set X} (hK : IsCompact K) (hB₀ : IsOpen B₀) (hKB : K⊆B₀)
    (A : n → n → Coeff) (W : n → L2Space) (a : n → Test)
    (hext : ∀ i,LocalEq Kᶜ (W i : Dist) (a i : Dist))
    (he : ∀ i,LocalEq B (planeDerivative (L (0,1)) (L (0,Complex.I)) (W i : Dist)+
      ∑ j,A i j • (W j : Dist)) 0)
    (g : X → ℂ) (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
    (hs : tsupport g⊆B) (h1 : EqOn g 1 B₀) :
    ∃ v : n → Test,(∀ i,(W i : Dist)=(v i : Dist)) ∧
      ∀ i,tsupport (v i-a i : Test)⊆K := by
…

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.L2Space, OAI.ElasticityDistribution.Test, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.planeDerivative

  28. def OAI.ElasticityDistribution.leadingPair line 460
  29. lemma OAI.ElasticityDistribution.lapd_null_direction line 465
  30. lemma OAI.ElasticityDistribution.normPair_null_leading line 473
  31. theorem OAI.ElasticityDistribution.leadingPair_matrix line 490

    Source documentation

    The physical leading equations have a scalar planar principal part on all four actual augmented entries. The constraint is retained separately.

    theorem leadingPair_matrix (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0)
    (lam m n o : Coeff) (hn : n*m=1) (ho : o*(lam+m+m)=1)
    (U : Fin 4 → Dist) (i : Fin 4) :
    leadingPair θ lam m n o U i=(2 : ℂ) • directiond θ (U i)+
      ∑ k,∑ j,θ k • (coeffA dc lam m n o k i j • U j) := by
…

    Mentions: OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.leadingPair, OAI.ElasticityDistribution.directiond, OAI.ElasticityDistribution.dc

  32. lemma OAI.ElasticityDistribution.leading_matrix_local line 511
  33. def OAI.ElasticityCoordinates.planeSplit line 532

    Source documentation

    The actual characteristic plane and its transverse kernel are complementary. No orthonormal-coordinate or slicing-existence premise is imposed.

    def planeSplit (J : ℂ →L[ℝ] E) (K : E →L[ℝ] ℂ) (hK : Function.LeftInverse K J) :
    E ≃L[ℝ] LinearMap.ker K.toLinearMap × ℂ :=
…
  34. lemma OAI.ElasticityCoordinates.planeSplit_symm line 562
  35. lemma OAI.ElasticityCoordinates.planeSplit_plane line 564
  36. lemma OAI.ElasticityCoordinates.planeSplit_symm_plane line 571
  37. lemma OAI.ElasticityDistribution.directiond_real_complex line 583
  38. lemma OAI.ElasticityDistribution.exists_direction_coordinates line 594
  39. lemma OAI.ElasticityDistribution.half_contraction line 612
  40. theorem OAI.ElasticityDistribution.weak_leading_smooth line 629

    Source documentation

    The actual weak leading augmented solution has a globally smooth representative; the compact exterior difference is preserved exactly.

    theorem weak_leading_smooth {K B B₀ : Set X} (hK : IsCompact K) (hB₀ : IsOpen B₀) (hKB : K⊆B₀)
    (θ : Fin 3 → ℂ) (hθ : ∑ i,θ i*θ i=0) (hne : θ≠0)
    (lam m n o : Coeff) (hn : n*m=1) (ho : o*(lam+m+m)=1)
    (W : Fin 4 → L2Space) (a : Fin 4 → Test)
    (hext : ∀ i,LocalEq Kᶜ (W i : Dist) (a i : Dist))
    (hr : ∀ i,LocalEq B (leadingRd θ lam m (fun j => (W j.succ : Dist)) (W 0 : Dist) i) 0)
    (hs : LocalEq B (leadingSd θ lam m (fun j => (W j.succ : Dist)) (W 0 : Dist)) 0)
    (g : X → ℂ) (hg : ContDiff ℝ (⊤ : ℕ∞) g) (hc : HasCompactSupport g)
    (hgs : tsupport g⊆B) (h1 : EqOn g 1 B₀) :
    ∃ v : Fin 4 → Test,(∀ i,(W i : Dist)=(v i : Dist)) ∧
      ∀ i,tsupport (v i-a i : Test)⊆K := by
…

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.L2Space, OAI.ElasticityDistribution.Test, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.leadingRd, OAI.ElasticityDistribution.leadingSd

  41. def OAI.ElasticityDistribution.schwartzDirection line 670
  42. def OAI.ElasticityDistribution.schwartzLeadingR line 671
  43. def OAI.ElasticityDistribution.schwartzLeadingS line 674
  44. lemma OAI.ElasticityDistribution.schwartzDirection_dist line 678
  45. lemma OAI.ElasticityDistribution.schwartzLeadingR_dist line 682
  46. lemma OAI.ElasticityDistribution.schwartzLeadingS_dist line 686
  47. lemma OAI.ElasticityDistribution.schwartzDirection_smooth line 690
  48. lemma OAI.ElasticityDistribution.direction_coeff_val line 694
  49. lemma OAI.ElasticityDistribution.toSmooth_coeff_mult line 698
  50. lemma OAI.ElasticityDistribution.dc_coeff_val line 701
  51. lemma OAI.ElasticityDistribution.schwartzLeadingR_smooth line 702
  52. lemma OAI.ElasticityDistribution.schwartzLeadingS_smooth line 707
  53. lemma OAI.ElasticityDistribution.leading_classical line 713
  54. lemma OAI.ElasticityCGO.localizedLeading_eqOn line 742
  55. lemma OAI.ElasticityDistribution.normal_classical line 765
  56. lemma OAI.ElasticityAugmented.direction_eqOn line 784
  57. lemma OAI.ElasticityAugmented.leadingR_eqOn line 791
  58. lemma OAI.ElasticityAugmented.leadingS_eqOn line 806
  59. theorem OAI.ElasticityDistribution.smooth_column_patch line 826

    Source documentation

    Patch the actual smooth representative to the original unlocalized amplitude, without pretending the localization derivative vanishes globally.

    theorem smooth_column_patch {K B : Set X} (hB : IsOpen B) (hKB : K⊆B)
    (θ : Fin 3 → ℂ) (lam m : Coeff) (v φ : Fin 4 → Test) (a₀ : Fin 4 → Smooth)
    (hs : ∀ i,tsupport (v i-φ i : Test)⊆K)
    (hφ : ∀ i,EqOn (φ i : X → ℂ) (a₀ i : X → ℂ) B)
    (hr : ∀ i,LocalEq B (leadingRd θ lam m (fun j => (v j.succ : Dist)) (v 0 : Dist) i) 0)
    (he : LocalEq B (leadingSd θ lam m (fun j => (v j.succ : Dist)) (v 0 : Dist)) 0)
    (hn : LocalEq B (normald θ (fun j => (v j.succ : Dist))) 0)
    (hn₀ : normal θ (fun j => a₀ j.succ)=0) :
    ∃ a : Fin 4 → Smooth,
      (∀ i,tsupport ((a i-a₀ i : Smooth) : X → ℂ)⊆K) ∧
      (∀ i,EqOn (leadingR (A := Smooth) coord θ lam.val m.val (fun j => a j.succ) (a 0) i : X → ℂ) 0 B) ∧
…

    Mentions: OAI.ElasticityDistribution.X, OAI.ElasticityDistribution.Coeff, OAI.ElasticityDistribution.Test, OAI.ElasticityDistribution.LocalEq, OAI.ElasticityDistribution.leadingRd, OAI.ElasticityDistribution.Dist, OAI.ElasticityDistribution.leadingSd, OAI.ElasticityDistribution.normald