OAI/MathematicalPhysics/Elasticity/BoundaryCharts.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Smooth boundary geometry in open partial homeomorphism charts.

  1. def OAI.Elasticity.SourceSmoothBoundary line 14
  2. def OAI.Elasticity.SourceDomain line 22
  3. lemma OAI.Elasticity.SourceSmoothBoundary.to_inherited line 25
  4. lemma OAI.Elasticity.SourceDomain.to_inherited line 31
  5. lemma OAI.Elasticity.chart_fderiv_left_inverse line 41
  6. lemma OAI.Elasticity.chart_fderiv_right_inverse line 51
  7. def OAI.Elasticity.chartDerivativeEquiv line 57

    Source documentation

    The derivative of a smooth open boundary chart is continuously invertible.

    def chartDerivativeEquiv : X ≃L[ℝ] X := {
…

    Mentions: OAI.Elasticity.X

  8. lemma OAI.Elasticity.chartDerivativeEquiv_apply line 70
  9. def OAI.Elasticity.coordinateNormal line 86

    Source documentation

    Normal covector of a linear boundary-coordinate map, represented in the fixed Euclidean coordinates by Riesz duality.

    def coordinateNormal (B : X ≃L[ℝ] X) : X :=
…

    Mentions: OAI.Elasticity.X

  10. lemma OAI.Elasticity.coordinateNormal_inner line 90
  11. lemma OAI.Elasticity.coordinateNormal_ne_zero line 94
  12. def OAI.Elasticity.coordinateFrame line 101

    Source documentation

    A physical orthogonal frame whose first vector is the inward normal.

    def coordinateFrame (B : X ≃L[ℝ] X) : X ≃ₗᵢ[ℝ] X :=
…

    Mentions: OAI.Elasticity.X

  13. lemma OAI.Elasticity.coordinateFrame_first line 104
  14. theorem OAI.Elasticity.coordinateFrame_normal line 114

    Source documentation

    This normalization preserves the physical half-space without changing its positive side. It also keeps the physical metric Euclidean at the base point.

    theorem coordinateFrame_normal (B : X ≃L[ℝ] X) (z : X) :
    B (coordinateFrame B z) 0 = ‖coordinateNormal B‖ * z 2 := by
…

    Mentions: OAI.Elasticity.X, OAI.Elasticity.coordinateFrame, OAI.Elasticity.coordinateNormal

  15. lemma OAI.Elasticity.coordinateFrame_positive line 129
  16. def OAI.Elasticity.normalizedLinear line 152
  17. def OAI.Elasticity.normalizedAffine line 156
  18. def OAI.Elasticity.normalizedParam line 159
  19. lemma OAI.Elasticity.normalizedAffine_apply line 162
  20. lemma OAI.Elasticity.normalizedParam_apply line 165
  21. lemma OAI.Elasticity.normalizedParam_source line 168
  22. lemma OAI.Elasticity.normalizedParam_target line 174
  23. lemma OAI.Elasticity.normalizedParam_zero_source line 179
  24. lemma OAI.Elasticity.normalizedParam_zero line 183
  25. lemma OAI.Elasticity.normalizedParam_contDiff line 186
  26. lemma OAI.Elasticity.normalizedParam_symm_contDiff line 196
  27. lemma OAI.Elasticity.normalizedParam_fderiv line 204
  28. lemma OAI.Elasticity.normalizedParam_halfspace line 224
  29. theorem OAI.Elasticity.SourceSmoothBoundary.normalized line 239

    Source documentation

    Normalized local physical parametrizations exist at every boundary point of a domain with smooth open boundary charts. No regularity is imposed on the Lamé moduli here.

    theorem SourceSmoothBoundary.normalized {Ω : Set X} (h : SourceSmoothBoundary Ω)
    {x : X} (hx : x ∈ frontier Ω) :
    ∃ (φ : OpenPartialHomeomorph X X) (Q : X ≃ₗᵢ[ℝ] X),
      (0 : X) ∈ φ.source ∧ φ 0 = x ∧
      ContDiffOn ℝ (⊤ : ℕ∞) φ φ.source ∧
      ContDiffOn ℝ (⊤ : ℕ∞) φ.symm φ.target ∧
      HasFDerivAt φ Q.toContinuousLinearEquiv.toContinuousLinearMap 0 ∧
      ∀ z ∈ φ.source, φ z ∈ Ω ↔ 0 < z 2 := by
…

    Mentions: OAI.Elasticity.X, OAI.Elasticity.SourceSmoothBoundary

  30. abbrev OAI.ElasticityBoundaryChartOperator.I line 267
  31. abbrev OAI.ElasticityBoundaryChartOperator.X line 268
  32. abbrev OAI.ElasticityBoundaryChartOperator.Y line 269
  33. def OAI.ElasticityBoundaryChartOperator.basis line 271
  34. def OAI.ElasticityBoundaryChartOperator.chartPrincipal line 273
  35. def OAI.ElasticityBoundaryChartOperator.chartLower line 278
  36. lemma OAI.ElasticityBoundaryChartOperator.smooth_jac line 284
  37. lemma OAI.ElasticityBoundaryChartOperator.smooth_hess line 288
  38. lemma OAI.ElasticityBoundaryChartOperator.smooth_chartPrincipal line 292
  39. lemma OAI.ElasticityBoundaryChartOperator.smooth_chartLower line 310
  40. lemma OAI.ElasticityBoundaryChartOperator.chartPrincipal_frozen line 337
  41. theorem OAI.ElasticityBoundaryChartOperator.physical_chart_operator line 365

    Source documentation

    Exact equality with the true physical stress divergence after pullback. The inverse chart equality is used literally, not replaced by a formal symbol.

    theorem physical_chart_operator (Q : X ≃ₗᵢ[ℝ] X) (Φ : Y → X) {ψ : X → Y}
    (hψ : ContDiff ℝ (⊤ : ℕ∞) ψ) {l m : X → ℂ}
    (hl : ContDiff ℝ (⊤ : ℕ∞) l) (hm : ContDiff ℝ (⊤ : ℕ∞) m)
    (u : I → Y → ℂ) (hu : ∀ j, ContDiff ℝ (⊤ : ℕ∞) (u j))
    (y : Y) (hy : ψ (Φ y)=y) (s : I) :
    (∑ i, frameMatrix Q i s*(∑ k, dd
      (stress basis l m (mix (frameMatrix Q) (fun j x => u j (ψ x))) i k) (basis k) (Φ y)))=
      strong (chartPrincipal Q Φ ψ l m) (chartLower Q Φ ψ l m) u s y := by
…

    Mentions: OAI.ElasticityBoundaryChartOperator.X, OAI.ElasticityBoundaryChartOperator.Y, OAI.ElasticityBoundaryChartOperator.I, OAI.ElasticityBoundaryChartOperator.basis, OAI.ElasticityBoundaryChartOperator.chartPrincipal, OAI.ElasticityBoundaryChartOperator.chartLower

  42. lemma OAI.ElasticityBoundary.contDiff_cutoff_smul line 398
  43. theorem OAI.ElasticityBoundary.smooth_vector_extension line 412

    Source documentation

    The output may itself be an actual chart or vector displacement.

    theorem smooth_vector_extension {K U : Set E} (hK : IsCompact K) (hU : IsOpen U)
    (hKU : K⊆U) (f : E → F) (hf : ContDiffOn ℝ (⊤ : ℕ∞) f U) :
    ∃ g : E → F, ContDiff ℝ (⊤ : ℕ∞) g ∧ HasCompactSupport g ∧ g =ᶠ[𝓝ˢ K] f := by
…
  44. def OAI.ElasticityBoundary.chartTransfer line 436
  45. lemma OAI.ElasticityBoundary.smooth_chartTransfer line 440
  46. lemma OAI.ElasticityBoundary.chartTransfer_apply line 449
  47. lemma OAI.ElasticityBoundary.chartTransfer_zero line 460
  48. lemma OAI.ElasticityBoundary.compact_chartTransfer line 467
  49. lemma OAI.ElasticityBoundary.chartTransfer_support line 472
  50. theorem OAI.ElasticityBoundary.compact_chart_data line 488

    Source documentation

    Cutoffs and both globally smooth chart extensions exist from honest source hypotheses. The extensions agree near the whole compact supports used in the physical change of variables.

    theorem compact_chart_data (e : OpenPartialHomeomorph E E)
    (he : ContDiffOn ℝ (⊤ : ℕ∞) e e.source)
    (hi : ContDiffOn ℝ (⊤ : ℕ∞) e.symm e.target)
    {K : Set E} (hK : IsCompact K) (hs : K⊆e.source) :
    ∃ (η : E → ℝ) (Φ Ψ : E → E),
      ContDiff ℝ (⊤ : ℕ∞) η ∧ HasCompactSupport η ∧ tsupport η⊆e.target ∧
      η =ᶠ[𝓝ˢ (e '' K)] (fun _ => 1) ∧
      ContDiff ℝ (⊤ : ℕ∞) Φ ∧ Φ =ᶠ[𝓝ˢ K] e ∧
      ContDiff ℝ (⊤ : ℕ∞) Ψ ∧ Ψ =ᶠ[𝓝ˢ (tsupport η)] e.symm := by
…
  51. abbrev OAI.ElasticityBoundaryOperatorLocal.I line 519
  52. lemma OAI.ElasticityBoundaryOperatorLocal.dd_germ line 522
  53. lemma OAI.ElasticityBoundaryOperatorLocal.dd_germ_eq line 527
  54. lemma OAI.ElasticityBoundaryOperatorLocal.directional_germ_eq line 530
  55. lemma OAI.ElasticityBoundaryOperatorLocal.directional_zero line 543
  56. lemma OAI.ElasticityBoundaryOperatorLocal.directional_support line 550
  57. lemma OAI.ElasticityBoundaryOperatorLocal.chartTransfer_germ line 566
  58. lemma OAI.ElasticityBoundaryOperatorLocal.chartTransfer_extension_germ line 575