OAI/MathematicalPhysics/Elasticity/BoundaryCalculus.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Literal first and second coordinate chain rules. The maps are genuine Frechet-smooth maps; a tensor pullback will use these identities, rather than postulating a transformed elasticity operator.

  1. abbrev OAI.ElasticityBoundaryChainRule.Y line 12
  2. def OAI.ElasticityBoundaryChainRule.dd line 15
  3. def OAI.ElasticityBoundaryChainRule.cp line 16
  4. def OAI.ElasticityBoundaryChainRule.jac line 17
  5. def OAI.ElasticityBoundaryChainRule.hess line 19
  6. lemma OAI.ElasticityBoundaryChainRule.smooth_dd line 22
  7. lemma OAI.ElasticityBoundaryChainRule.smooth_jac line 26
  8. lemma OAI.ElasticityBoundaryChainRule.fderiv_basis line 30
  9. lemma OAI.ElasticityBoundaryChainRule.dd_comp line 44
  10. lemma OAI.ElasticityBoundaryChainRule.dd_sum line 51
  11. lemma OAI.ElasticityBoundaryChainRule.dd_mul line 57
  12. lemma OAI.ElasticityBoundaryChainRule.dd_ofReal line 63
  13. theorem OAI.ElasticityBoundaryChainRule.dd_dd_comp line 69

    Source documentation

    The second chain rule with the exact Hessian-of-coordinate lower term.

    theorem dd_dd_comp {f : Y → ℂ} {ψ : E → Y}
    (hf : ContDiff ℝ (⊤ : ℕ∞) f) (hψ : ContDiff ℝ (⊤ : ℕ∞) ψ) (v w x : E) :
    dd (dd (fun z => f (ψ z)) w) v x=
      (∑ β, (hess ψ v w β x:ℂ)*cp f β (ψ x))+
      ∑ β, ∑ α, (jac ψ w β x:ℂ)*(jac ψ v α x:ℂ)*cp (cp f β) α (ψ x) := by
…

    Mentions: OAI.ElasticityBoundaryChainRule.Y, OAI.ElasticityBoundaryChainRule.dd, OAI.ElasticityBoundaryChainRule.hess, OAI.ElasticityBoundaryChainRule.cp, OAI.ElasticityBoundaryChainRule.jac

  14. abbrev OAI.ElasticityBoundaryMVCalculus.Y line 105
  15. abbrev OAI.ElasticityBoundaryMVCalculus.MP line 106
  16. def OAI.ElasticityBoundaryMVCalculus.complexCoord line 108
  17. lemma OAI.ElasticityBoundaryMVCalculus.complexCoord_apply line 111
  18. def OAI.ElasticityBoundaryMVCalculus.value line 113
  19. lemma OAI.ElasticityBoundaryMVCalculus.value_C line 115
  20. lemma OAI.ElasticityBoundaryMVCalculus.value_X line 116
  21. lemma OAI.ElasticityBoundaryMVCalculus.value_zero line 117
  22. lemma OAI.ElasticityBoundaryMVCalculus.value_one line 118
  23. lemma OAI.ElasticityBoundaryMVCalculus.value_add line 119
  24. lemma OAI.ElasticityBoundaryMVCalculus.value_sub line 120
  25. lemma OAI.ElasticityBoundaryMVCalculus.value_mul line 121
  26. lemma OAI.ElasticityBoundaryMVCalculus.value_smul line 122
  27. lemma OAI.ElasticityBoundaryMVCalculus.value_C_fn line 125
  28. lemma OAI.ElasticityBoundaryMVCalculus.value_add_fn line 126
  29. lemma OAI.ElasticityBoundaryMVCalculus.value_mul_fn line 127
  30. lemma OAI.ElasticityBoundaryMVCalculus.value_X_fn line 128
  31. lemma OAI.ElasticityBoundaryMVCalculus.smooth_value line 130
  32. def OAI.ElasticityBoundaryMVCalculus.differential line 136
  33. lemma OAI.ElasticityBoundaryMVCalculus.differential_C line 139
  34. lemma OAI.ElasticityBoundaryMVCalculus.differential_add line 144
  35. lemma OAI.ElasticityBoundaryMVCalculus.differential_mul_X line 150
  36. theorem OAI.ElasticityBoundaryMVCalculus.hasFDerivAt_value line 170

    Source documentation

    The evaluated formal partial derivatives are the actual Frechet derivative.

    theorem hasFDerivAt_value (p : MP) (y : Y) : HasFDerivAt (value p) (differential p y) y := by
…

    Mentions: OAI.ElasticityBoundaryMVCalculus.MP, OAI.ElasticityBoundaryMVCalculus.Y, OAI.ElasticityBoundaryMVCalculus.value, OAI.ElasticityBoundaryMVCalculus.differential

  37. lemma OAI.ElasticityBoundaryMVCalculus.differential_basis line 178
  38. theorem OAI.ElasticityBoundaryMVCalculus.fderiv_value_basis line 182
  39. theorem OAI.ElasticityBoundaryMVCalculus.polynomialGrowth line 188

    Source documentation

    Every fixed amplitude is bounded by a uniform polynomial moment, so the Gaussian/exponential majorants used for its remainder are honest integrable functions.

    theorem polynomialGrowth (p : MP) :
    ∃ C : ℝ, 0 ≤ C ∧ ∃ d : ℕ, ∀ y : Y, ‖value p y‖ ≤ C*(1+‖y‖)^d := by
…

    Mentions: OAI.ElasticityBoundaryMVCalculus.MP, OAI.ElasticityBoundaryMVCalculus.Y, OAI.ElasticityBoundaryMVCalculus.value

  40. abbrev OAI.ElasticityBoundaryScaling.Y line 227
  41. def OAI.ElasticityBoundaryScaling.scaleFactor line 229
  42. def OAI.ElasticityBoundaryScaling.scale line 231
  43. lemma OAI.ElasticityBoundaryScaling.scale_apply line 235
  44. lemma OAI.ElasticityBoundaryScaling.scale_zero line 238
  45. lemma OAI.ElasticityBoundaryScaling.scale_comp line 242
  46. lemma OAI.ElasticityBoundaryScaling.scale_one line 247
  47. lemma OAI.ElasticityBoundaryScaling.scale_inv line 251
  48. lemma OAI.ElasticityBoundaryScaling.scale_injective line 254
  49. lemma OAI.ElasticityBoundaryScaling.scale_surjective line 259
  50. lemma OAI.ElasticityBoundaryScaling.scale_det line 262
  51. lemma OAI.ElasticityBoundaryScaling.scale_norm_le line 269
  52. lemma OAI.ElasticityBoundaryScaling.continuous_scale_at line 282
  53. lemma OAI.ElasticityBoundaryScaling.scale_tendsto_zero line 288
  54. theorem OAI.ElasticityBoundaryScaling.integral_scale line 295

    Source documentation

    Exact full-space change of variables; valid even when the integral is the Bochner fallback zero, and for vector-valued functions.

    theorem integral_scale {δ : ℝ} (hδ : δ≠0) (f : Y → F) :
    (∫ y, f y) = δ^4 • ∫ y, f (scale δ y) := by
…

    Mentions: OAI.ElasticityBoundaryScaling.Y, OAI.ElasticityBoundaryScaling.scale

  55. lemma OAI.ElasticityBoundaryScaling.scaled_integrable_iff line 304
  56. abbrev OAI.ElasticityBoundaryWeights.Y line 325
  57. def OAI.ElasticityBoundaryWeights.factor line 327
  58. def OAI.ElasticityBoundaryWeights.weight line 331
  59. lemma OAI.ElasticityBoundaryWeights.factor_nonneg line 333
  60. lemma OAI.ElasticityBoundaryWeights.weight_nonneg line 339
  61. lemma OAI.ElasticityBoundaryWeights.measurable_factor line 342
  62. lemma OAI.ElasticityBoundaryWeights.measurable_weight line 350
  63. lemma OAI.ElasticityBoundaryWeights.integrable_factor_pow line 354
  64. lemma OAI.ElasticityBoundaryWeights.integrable_factor line 375
  65. lemma OAI.ElasticityBoundaryWeights.integrable_weight line 378
  66. lemma OAI.ElasticityBoundaryWeights.integrable_coordinate_moment line 381
  67. lemma OAI.ElasticityBoundaryWeights.norm_pow_le_sum line 392
  68. theorem OAI.ElasticityBoundaryWeights.integrable_norm_moment line 399

    Source documentation

    Every finite radial moment of the Gaussian-tangential, exponential-normal profile is integrable over the full coordinate space (zero for t≤0).

    theorem integrable_norm_moment {b : ℝ} (hb : 0 < b) (n : ℕ) :
    Integrable (fun y : Y => ‖y‖^n * weight b y) := by
…

    Mentions: OAI.ElasticityBoundaryWeights.Y, OAI.ElasticityBoundaryWeights.weight