OAI/Analysis/Conductivity/Flux/PhysicalSplicedGreen.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.PhysicalFiniteEndingData.flatTensor line 15
  2. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.correctedEndJet_parent line 17
  3. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.correctedEndJet_child line 24
  4. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_child_energy_pullback line 33
  5. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_parent_jet_green line 69
  6. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_child_jet_green line 89
  7. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_jet_green line 108
  8. def OAI.ScalarConductivity.constantTerminalFluxCLM line 131
  9. lemma OAI.ScalarConductivity.constantTerminalFlux_smooth line 136
  10. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.flatTensor_properties line 151
  11. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_gradient line 159
  12. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_end_smooth_green line 167
  13. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_block_smooth_green line 188
  14. lemma OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_block_green line 205
  15. theorem OAI.ScalarConductivity.PhysicalFiniteEndingData.corrected_pair_green_exists line 219