OAI/Geometry/IsometricImmersion/Energy/HyperbolicEnergyDensity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Hyperbolic.hyperbolicOperator line 13
  2. def OAI.SmoothLocal.Hyperbolic.energyDensity line 18
  3. def OAI.SmoothLocal.Hyperbolic.energyFlux line 21
  4. def OAI.SmoothLocal.Hyperbolic.energyCoefficientError line 25
  5. theorem OAI.SmoothLocal.Hyperbolic.energyDensity_partial_theta line 32
  6. theorem OAI.SmoothLocal.Hyperbolic.energyFlux_partial_xi line 50
  7. theorem OAI.SmoothLocal.Hyperbolic.energy_density_flux_identity line 70
  8. theorem OAI.SmoothLocal.Hyperbolic.energy_fields_contDiffOn line 85
  9. theorem OAI.SmoothLocal.Hyperbolic.energyDensity_nonneg line 102
  10. theorem OAI.SmoothLocal.Hyperbolic.scalar_flux_bound line 106
  11. theorem OAI.SmoothLocal.Hyperbolic.energyFlux_abs_le line 134
  12. theorem OAI.SmoothLocal.Hyperbolic.inward_boundary_nonpositive line 138
  13. theorem OAI.SmoothLocal.Hyperbolic.scalar_coefficient_error_bound line 152
  14. theorem OAI.SmoothLocal.Hyperbolic.energyCoefficientError_abs_le line 189