OAI/MathematicalPhysics/Boltzmann/Compactness/NormalizedKernelAction.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

The normalized Carleman gain as a measurable velocity kernel

  1. def OAI.BoltzmannNonuniqueness.ChartKernel.coordinateKernel line 29
  2. instance OAI.BoltzmannNonuniqueness.ChartKernel.coordinateKernel_sFinite line 34
  3. theorem OAI.BoltzmannNonuniqueness.ChartKernel.coordinateKernel_apply line 41
  4. def OAI.BoltzmannNonuniqueness.ChartKernel.inputMeasure line 47
  5. theorem OAI.BoltzmannNonuniqueness.ChartKernel.inputMeasure_measurable line 50
  6. def OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel line 69
  7. theorem OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel_mass line 74
  8. theorem OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel_eq_map line 99
  9. instance OAI.BoltzmannNonuniqueness.ChartKernel.inputKernel_sFinite line 110
  10. theorem OAI.BoltzmannNonuniqueness.ChartKernel.lintegral_inputKernel line 115
  11. theorem OAI.BoltzmannNonuniqueness.ChartKernel.measure_weighted line 142
  12. theorem OAI.BoltzmannNonuniqueness.ChartKernel.lintegral_normalized line 154
  13. theorem OAI.BoltzmannNonuniqueness.ChartKernel.lintegral_inputKernel_eq_gain line 168
  14. theorem OAI.BoltzmannNonuniqueness.chartGain_const_mul_right line 193
  15. theorem OAI.BoltzmannNonuniqueness.normalized_integral_eq line 206
  16. theorem OAI.BoltzmannNonuniqueness.normalized_integral_congr_ae line 219
  17. def OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor line 252
  18. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor_measurable line 255
  19. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor_fiber_integral line 262
  20. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor_integrable line 268
  21. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor_L1_le line 295
  22. theorem OAI.BoltzmannNonuniqueness.ChartKernel.normalized_weight_gain_bound line 338
  23. theorem OAI.BoltzmannNonuniqueness.ChartKernel.normalized_weight_scaled_bound line 349
  24. theorem OAI.BoltzmannNonuniqueness.Compactness.tendstoInMeasure_continuous_comp line 375
  25. theorem OAI.BoltzmannNonuniqueness.Compactness.normalized_product_bound line 387
  26. theorem OAI.BoltzmannNonuniqueness.Compactness.tendsto_L1_normalized_product line 396
  27. def OAI.BoltzmannNonuniqueness.Compactness.fiberMass line 463
  28. def OAI.BoltzmannNonuniqueness.Compactness.normalizedPair line 465
  29. theorem OAI.BoltzmannNonuniqueness.Compactness.fiberMass_measurable line 468
  30. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedTensor_norm_swap line 471
  31. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_integrable line 486
  32. theorem OAI.BoltzmannNonuniqueness.Compactness.normalizedPair_truncation_error line 493
  33. def OAI.BoltzmannNonuniqueness.ChartKernel.action line 545
  34. theorem OAI.BoltzmannNonuniqueness.ChartKernel.action_measurable line 548
  35. theorem OAI.BoltzmannNonuniqueness.ChartKernel.action_normalized_congr_ae line 554