OAI/MathematicalPhysics/Elasticity/BoundaryValues.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Strictly positive Gaussian-normal moments, without relying on a numerical constant or an unproved nondegeneracy of the boundary limit.

  1. lemma OAI.ElasticityBoundaryWeights.weight_zero_of_nonpos line 13
  2. lemma OAI.ElasticityBoundaryWeights.weight_pos line 16
  3. def OAI.ElasticityBoundaryWeights.normalMoment line 19
  4. lemma OAI.ElasticityBoundaryWeights.normal_moment_integrable line 21
  5. lemma OAI.ElasticityBoundaryWeights.normalMoment_pos line 29
  6. lemma OAI.ElasticityBoundaryWeights.normalMoment_complex line 40
  7. lemma OAI.ElasticityBoundaryPacket.polynomial_bound line 64
  8. lemma OAI.ElasticityBoundaryPacket.weighted_integrable line 68
  9. lemma OAI.ElasticityBoundaryPacket.frozen_integrable line 87
  10. lemma OAI.ElasticityBoundaryPacket.frozenPair_integral line 97
  11. lemma OAI.ElasticityBoundaryPacket.frozenPair_constant line 119
  12. abbrev OAI.ElasticityBoundaryLeading.I line 141
  13. abbrev OAI.ElasticityBoundaryLeading.Y line 142
  14. def OAI.ElasticityBoundaryLeading.leading line 144
  15. def OAI.ElasticityBoundaryLeading.grad line 146
  16. lemma OAI.ElasticityBoundaryLeading.leading_normal line 148
  17. lemma OAI.ElasticityBoundaryLeading.leading_apply line 154
  18. lemma OAI.ElasticityBoundaryLeading.grad_leading line 158
  19. lemma OAI.ElasticityBoundaryLeading.tensorDensity_factor line 165
  20. lemma OAI.ElasticityBoundaryLeading.transverse_density line 169
  21. lemma OAI.ElasticityBoundaryLeading.longitudinal_trace line 177
  22. lemma OAI.ElasticityBoundaryLeading.longitudinal_density line 184
  23. lemma OAI.ElasticityBoundaryLeading.longitudinal_trace_ne line 193
  24. lemma OAI.ElasticityBoundaryPacket.pair_separates line 210
  25. lemma OAI.ElasticityBoundaryPacket.elasticityTensor_sub line 255
  26. lemma OAI.ElasticityBoundaryPacket.admissible_frozen_ne line 261
  27. lemma OAI.ElasticityBoundaryPacket.Setup.boundary_values line 269
  28. lemma OAI.ElasticityBoundaryPacket.boundary_values_global line 308
  29. abbrev OAI.ElasticityBoundaryNormalTaylor.Y line 328
  30. def OAI.ElasticityBoundaryNormalTaylor.en line 330
  31. def OAI.ElasticityBoundaryNormalTaylor.projection line 332
  32. def OAI.ElasticityBoundaryNormalTaylor.travel line 334
  33. lemma OAI.ElasticityBoundaryNormalTaylor.en_apply_two line 336
  34. lemma OAI.ElasticityBoundaryNormalTaylor.projection_two line 337
  35. lemma OAI.ElasticityBoundaryNormalTaylor.projection_zero line 338
  36. lemma OAI.ElasticityBoundaryNormalTaylor.travel_zero line 339
  37. lemma OAI.ElasticityBoundaryNormalTaylor.travel_one line 340
  38. def OAI.ElasticityBoundaryNormalTaylor.normalJet line 344
  39. def OAI.ElasticityBoundaryNormalTaylor.quotient line 347
  40. lemma OAI.ElasticityBoundaryNormalTaylor.normalJet_continuous line 351
  41. lemma OAI.ElasticityBoundaryNormalTaylor.travel_continuous line 356
  42. lemma OAI.ElasticityBoundaryNormalTaylor.quotient_continuous line 361
  43. lemma OAI.ElasticityBoundaryNormalTaylor.normal_factor line 374
  44. lemma OAI.ElasticityBoundaryNormalTaylor.quotient_zero line 396