OAI/MathematicalPhysics/Boltzmann/Branching/RedundantParameterSupport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The redundant coordinates recover the actual graph-chart velocity

  1. def OAI.BoltzmannNonuniqueness.RedundantPlane.normalVector line 23
  2. def OAI.BoltzmannNonuniqueness.RedundantPlane.crossVelocity line 25
  3. def OAI.BoltzmannNonuniqueness.RedundantPlane.tangentOffset line 28
  4. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normal_norm_sq line 31
  5. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.crossVelocity_on_plane line 35
  6. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.crossVelocity_axial line 40
  7. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.crossVelocity_tangent line 44
  8. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.chart_crossVelocity line 51
  9. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.chart_integral_redundant line 96
  10. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.gain_redundant line 121
  11. def OAI.BoltzmannNonuniqueness.RedundantPlane.normalCoefficient line 153
  12. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.measurable_redundant_point line 156
  13. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.measurable_normalCoefficient line 165
  14. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.ae_normal_ne line 171
  15. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.gain_density_redundant line 180
  16. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.inputKernel_redundant line 189
  17. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.normSq_eq_norm_sq line 221
  18. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.plane_parameter_sq_bound line 225
  19. theorem OAI.BoltzmannNonuniqueness.RedundantPlane.plane_parameter_bound line 256