OAI/Analysis/Conductivity/Sobolev/OriginalSmoothMultiplier.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.originalMulComponentCLM line 15
  2. def OAI.ScalarConductivity.originalMulJetCLM line 21
  3. lemma OAI.ScalarConductivity.originalMulComponentCLM_value line 24
  4. lemma OAI.ScalarConductivity.originalMulComponentCLM_gradient line 30
  5. lemma OAI.ScalarConductivity.originalMulJetCLM_ae line 48
  6. lemma OAI.ScalarConductivity.originalMulJetCLM_smooth line 60
  7. lemma OAI.ScalarConductivity.originalMulJetCLM_mem_zero line 82
  8. theorem OAI.ScalarConductivity.original_smooth_mul_exists line 96
  9. lemma OAI.ScalarConductivity.LocalLipAt.add line 113
  10. def OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileParent line 122
  11. def OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileChild line 126
  12. def OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfile line 131
  13. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalTime_locallyLipschitz line 134
  14. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileParent_localLip line 139
  15. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileChild_localLip line 148
  16. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfile_localLip line 159
  17. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileParent_zero_left line 166
  18. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileParent_zero_right line 170
  19. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfileChild_zero line 175
  20. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalTime_far_parent line 180
  21. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfile_zero_outside line 187
  22. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfile_H10 line 199
  23. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfile_parent_band line 212
  24. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.terminalProfile_child_band line 225