OAI/MathematicalPhysics/Boltzmann/Jets/GeometricLocalizedEntry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Local density normalization cancels from the actual beam measure and frequency

  1. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scaled_beamDensity line 30
  2. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scaled_beamMeasure line 37
  3. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scaled_characteristicBeamFrequency line 49
  4. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamPartner_norm_le_two line 79
  5. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_finite_gain_endpoint_le line 90
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicHistoryCore line 129
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.characteristicHistoryCore_measurable line 132
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.boundedFlightCone_mem_historyCore line 139
  9. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_history_cone_conditions line 149
  10. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_history_domination line 203
  11. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.geometric_localized_block_growth line 244
  12. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scaledBeamNormalKernel_independent line 319
  13. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamNormalRetainedKernel_independent line 342
  14. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.localized_three_entry_positive line 372