OAI/MathematicalPhysics/Elasticity/BoundaryJets.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Projection-stable packet supports are constructed inside honest open charts.

  1. lemma OAI.ElasticityBoundaryPacket.setup_ball_exists line 14
  2. lemma OAI.ElasticityBoundaryPacket.projection_norm_le line 60
  3. lemma OAI.ElasticityBoundaryPacket.projection_mem line 72
  4. lemma OAI.ElasticityBoundaryFlatComposition.comp_flat line 90
  5. lemma OAI.ElasticityBoundaryPacket.Setup.plane_frontier line 116
  6. def OAI.ElasticityBoundaryPacket.Setup.chartFunction line 135
  7. lemma OAI.ElasticityBoundaryPacket.Setup.chartFunction_smooth line 138
  8. lemma OAI.ElasticityBoundaryPacket.Setup.chart_flat line 142
  9. lemma OAI.ElasticityBoundaryPacket.Setup.chart_normal_factor line 153
  10. lemma OAI.ElasticityBoundaryPacket.elasticityTensor_decomp line 182
  11. lemma OAI.ElasticityBoundaryPacket.Setup.rawCoeff_decomp line 188
  12. def OAI.ElasticityBoundaryPacket.Setup.linearCoeff line 201
  13. lemma OAI.ElasticityBoundaryPacket.Setup.linearCoeff_continuous line 205
  14. lemma OAI.ElasticityBoundaryPacket.Setup.linearCoeff_zero line 211
  15. lemma OAI.ElasticityBoundaryPacket.Setup.localize_linearCoeff line 216
  16. lemma OAI.ElasticityBoundaryPacket.Setup.boundary_normal_step line 252
  17. def OAI.ElasticityBoundaryJetSymmetry.dir line 319
  18. def OAI.ElasticityBoundaryJetSymmetry.word line 321
  19. lemma OAI.ElasticityBoundaryJetSymmetry.dir_smooth line 325
  20. lemma OAI.ElasticityBoundaryJetSymmetry.word_smooth line 329
  21. lemma OAI.ElasticityBoundaryJetSymmetry.dir_comm line 335
  22. lemma OAI.ElasticityBoundaryJetSymmetry.word_perm line 351
  23. lemma OAI.ElasticityBoundaryJetSymmetry.word_ofFn line 359
  24. lemma OAI.ElasticityBoundaryJetSymmetry.iterated_perm line 374
  25. lemma OAI.ElasticityBoundaryFlatHyperplane.tangent_deriv_zero line 394
  26. lemma OAI.ElasticityBoundaryFlatHyperplane.flat_step line 407
  27. lemma OAI.ElasticityBoundaryPacket.Setup.chart_full_step line 455
  28. lemma OAI.ElasticityBoundaryPacket.Setup.Ψ_zero line 469
  29. lemma OAI.ElasticityBoundaryPacket.Setup.inverse_germ line 474
  30. lemma OAI.ElasticityBoundaryPacket.Setup.physical_flat_of_chart line 485
  31. lemma OAI.ElasticityBoundaryPacket.boundary_flat_difference_global line 519
  32. lemma OAI.ElasticityBoundaryPacket.boundary_jets_global line 568
  33. lemma OAI.ElasticityBoundaryPacket.admissible_boundary_values line 605
  34. theorem OAI.ElasticityBoundaryPacket.admissible_boundary_jets line 643