OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RawDensitySample.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal bounded samples of the actual unnormalized three-dimensional localized density, including the irrational fixed transverse frequency.

  1. abbrev OAI.ContinuumCoulomb.RawDensitySample.Input line 16
  2. def OAI.ContinuumCoulomb.RawDensitySample.planarArgument line 18
  3. def OAI.ContinuumCoulomb.RawDensitySample.verticalArgument line 21
  4. def OAI.ContinuumCoulomb.RawDensitySample.value line 23
  5. theorem OAI.ContinuumCoulomb.RawDensitySample.value_nonnegative line 27
  6. theorem OAI.ContinuumCoulomb.RawDensitySample.value_le_one line 30
  7. theorem OAI.ContinuumCoulomb.RawDensitySample.position_split line 36
  8. theorem OAI.ContinuumCoulomb.RawDensitySample.planar_norm_le line 44
  9. theorem OAI.ContinuumCoulomb.RawDensitySample.unit_product_error line 55
  10. theorem OAI.ContinuumCoulomb.RawDensitySample.value_error line 67