OAI/Dynamics/TriangleBilliards/SmoothingLp.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularBilliards.double_lintegral_assoc line 21
  2. lemma OAI.TriangularBilliards.directS_stronglyMeasurable line 31
  3. lemma OAI.TriangularBilliards.reflectedS_stronglyMeasurable line 42
  4. lemma OAI.TriangularBilliards.reflectedSmoothing_stronglyMeasurable line 56
  5. lemma OAI.TriangularBilliards.directS_l2sq line 65
  6. lemma OAI.TriangularBilliards.measurePreserving_directionParityReflection line 89
  7. lemma OAI.TriangularBilliards.reflectedS_l2sq line 99
  8. lemma OAI.TriangularBilliards.eLpNorm_two_mono_lintegral line 131
  9. lemma OAI.TriangularBilliards.directS_eLpNorm line 139
  10. lemma OAI.TriangularBilliards.reflectedS_eLpNorm line 150
  11. lemma OAI.TriangularBilliards.reflectedSmoothing_eLpNorm line 161
  12. lemma OAI.TriangularBilliards.reflectedSmoothing_memLp line 181
  13. def OAI.TriangularBilliards.directGradS line 188

    Source documentation

    The actual gradient convolution, as a bounded linear differential.

    def directGradS (Q : Triangle) (ε : ℝ) (f : SmoothPhase → ℂ) : SmoothPhase → (ℂ →L[ℝ] ℂ) :=
…

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.SmoothPhase

  14. def OAI.TriangularBilliards.reflectedGradS line 191
  15. def OAI.TriangularBilliards.reflectedSmoothingGradient line 196
  16. lemma OAI.TriangularBilliards.derivative_kernel_row_bound line 199
  17. lemma OAI.TriangularBilliards.derivative_kernel_col_bound line 209
  18. lemma OAI.TriangularBilliards.reflected_derivative_kernel_row_bound line 219
  19. lemma OAI.TriangularBilliards.reflected_derivative_kernel_col_bound line 234
  20. lemma OAI.TriangularBilliards.smulRight_stronglyMeasurable line 239
  21. lemma OAI.TriangularBilliards.directGradS_stronglyMeasurable line 245
  22. lemma OAI.TriangularBilliards.reflectedGradS_stronglyMeasurable line 256
  23. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_stronglyMeasurable line 271
  24. lemma OAI.TriangularBilliards.eLpNorm_two_le_of_lintegral line 277
  25. lemma OAI.TriangularBilliards.directGradS_l2sq line 292
  26. lemma OAI.TriangularBilliards.reflectedGradS_l2sq line 322
  27. lemma OAI.TriangularBilliards.directGradS_eLpNorm line 360
  28. lemma OAI.TriangularBilliards.reflectedGradS_eLpNorm line 371
  29. lemma OAI.TriangularBilliards.eLpNorm_add_sum_fin_three_le line 382
  30. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_eLpNorm line 403
  31. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_memLp line 415