OAI/Analysis/Steinitz/SectionEnergy.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Heat and energy inequalities for affine sections.

  1. def OAI.HeatL2.complexLp line 15
  2. lemma OAI.HeatL2.complexLp_coe line 18
  3. lemma OAI.HeatL2.complexLp_norm_sq line 21
  4. def OAI.HeatL2.nonnegRepresentative line 28
  5. lemma OAI.HeatL2.nonnegRepresentative_measurable line 31
  6. lemma OAI.HeatL2.nonnegRepresentative_nonneg line 35
  7. lemma OAI.HeatL2.nonnegRepresentative_zero line 39
  8. lemma OAI.HeatL2.nonnegRepresentative_ae line 42
  9. lemma OAI.HeatL2.nonnegRepresentative_memLp line 49
  10. lemma OAI.HeatL2.nonnegRepresentative_square line 53
  11. def OAI.HeatL2.realDistance line 68
  12. lemma OAI.HeatL2.realDistance_eq line 70
  13. lemma OAI.HeatL2.realDistance_integrable line 82
  14. lemma OAI.HeatL2.realEnergy_eq line 87
  15. lemma OAI.HeatL2.norm_representative_distance_le line 93
  16. lemma OAI.HeatL2.horizontal_translate_preserving line 126
  17. lemma OAI.HeatL2.horizontal_difference_integrable line 131
  18. lemma OAI.HeatL2.slice_memLp line 146
  19. def OAI.HeatL2.sliceEnergy line 153
  20. lemma OAI.HeatL2.sliceEnergy_integrable line 156
  21. lemma OAI.HeatL2.integral_sliceEnergy line 169
  22. lemma OAI.HeatL2.integral_sliceEnergy_le line 193
  23. def OAI.ShiftedSections.sliceMass line 216
  24. lemma OAI.ShiftedSections.sliceMass_nonneg line 219
  25. lemma OAI.ShiftedSections.sliceMass_integrable line 222
  26. lemma OAI.ShiftedSections.integral_sliceMass line 226
  27. lemma OAI.ShiftedSections.sliceMass_height_integrable line 231
  28. lemma OAI.ShiftedSections.integral_sliceMass_height line 237
  29. lemma OAI.ShiftedSections.height_above_one line 243
  30. lemma OAI.ShiftedSections.activeHeights_contains_one line 265
  31. lemma OAI.ShiftedSections.activeHeights_lt line 273
  32. lemma OAI.HeatL2.loss_bounded_lower line 288
  33. lemma OAI.HeatL2.compressed_norm_smalltime line 305
  34. lemma OAI.HeatL2.energy_lower_rate line 316
  35. lemma OAI.HeatL2.energy_lower_affine line 334
  36. lemma OAI.ShiftedSections.sliceMass_affine_integrable line 360
  37. lemma OAI.ShiftedSections.integral_sliceMass_affine line 370
  38. lemma OAI.ShiftedSections.integrated_section_rate line 381
  39. lemma OAI.HeatL2.energy_sum_dilate_le line 447
  40. lemma OAI.HeatL2.norm_representative_energy_le line 469
  41. lemma OAI.HeatL2.Diagonal.directionalSymbol_single line 481
  42. lemma OAI.HeatL2.Diagonal.symbol_scaled_sum line 486
  43. lemma OAI.HeatL2.Diagonal.energy_weighted_le line 496
  44. lemma OAI.HeatL2.Diagonal.norm_representative_diagonal_energy_le line 517
  45. lemma OAI.HeatL2.Diagonal.simultaneous_real_density line 536
  46. lemma OAI.HeatL2.Diagonal.real_coordinate_distance line 554
  47. lemma OAI.HeatL2.Diagonal.energy_weighted_density line 577
  48. lemma OAI.HeatL2.Diagonal.exists_coordinate_time line 595