OAI/Dynamics/TriangleBilliards/SmoothingApproximation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_fderiv_neg line 21
2. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_fderiv_integral line 32
3. lemma OAI.TriangularBilliards.SpatialSmoothing.rho_smulRight_integral line 41
4. lemma OAI.TriangularBilliards.SpatialSmoothing.rescaled_gradient_continuous line 49
5. lemma OAI.TriangularBilliards.SpatialSmoothing.rescaled_gradient_dominated line 58
6. lemma OAI.TriangularBilliards.SpatialSmoothing.rescaled_gradient_pointwise line 63
7. lemma OAI.TriangularBilliards.SpatialSmoothing.rescaled_gradient_tendsto line 77

   Source documentation

   Rescaled cancellation for a bounded spatially continuous input. This is the elementary pointwise producer for the small scaled derivative.

   lemma rescaled_gradient_tendsto (f : ℂ →ᵇ ℂ) (x : ℂ) :
       Tendsto (fun ε : ℝ => ∫ y : ℂ,
         (fderiv ℝ rho y).smulRight (f (x - ε • y))) (𝓝 0) (𝓝 0) := by
   …

   Mentions: OAI.TriangularBilliards.SpatialSmoothing.rho

8. lemma OAI.TriangularBilliards.SpatialSmoothing.scaled_full_gradient line 95

   Source documentation

   Exact substitution relating the rescaled derivative to the actual first-derivative convolution kernel.

   lemma scaled_full_gradient (ε : ℝ) (hε : 0 < ε) (f : ℂ → ℂ) (x : ℂ) :
       ε • (∫ y : ℂ, (fderiv ℝ (kernel ε) (x-y)).smulRight (f y)) =
         ∫ y : ℂ, (fderiv ℝ rho y).smulRight (f (x - ε • y)) := by
   …

   Mentions: OAI.TriangularBilliards.SpatialSmoothing.kernel, OAI.TriangularBilliards.SpatialSmoothing.rho

9. lemma OAI.TriangularBilliards.kernel_fderiv_eq_zero line 126
10. lemma OAI.TriangularBilliards.directGradS_eq_full line 133
11. lemma OAI.TriangularBilliards.reflectedGradS_zero_of_coord line 148
12. lemma OAI.TriangularBilliards.eventually_interior_gradient line 159
13. lemma OAI.TriangularBilliards.scaled_gradient_pointwise line 181
14. lemma OAI.TriangularBilliards.norm_integral_le_kernel_bound line 198
15. lemma OAI.TriangularBilliards.directGradS_norm_bound line 212
16. lemma OAI.TriangularBilliards.reflectedGradS_norm_bound line 224
17. lemma OAI.TriangularBilliards.scaled_gradient_norm_bound line 236
18. lemma OAI.TriangularBilliards.ae_double_position_in_table line 254
19. lemma OAI.TriangularBilliards.scaled_gradient_integral_tendsto line 261

    Source documentation

    The small-scaled-derivative estimate on the dense class of bounded continuous fields, for the actual reflected convolution kernel.

    lemma scaled_gradient_integral_tendsto (Q : Triangle) (f : DoublePhase →ᵇ ℂ) :
        Tendsto (fun ε : ℝ => ∫ z, ‖ε • reflectedSmoothingGradient Q ε f z‖ ^ 2 ∂doubleMeasure Q)
          (𝓝[>] 0) (𝓝 0) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.reflectedSmoothingGradient, OAI.TriangularBilliards.doubleMeasure

20. lemma OAI.TriangularBilliards.integrable_slice_ae line 285
21. lemma OAI.TriangularBilliards.equal_slice_ae line 302
22. lemma OAI.TriangularBilliards.directGradS_congr_ae line 319
23. lemma OAI.TriangularBilliards.reflectedGradS_congr_ae line 326
24. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_congr_ae line 335
25. lemma OAI.TriangularBilliards.smulRight_sub line 346
26. lemma OAI.TriangularBilliards.smulRight_integrable line 352
27. lemma OAI.TriangularBilliards.directGradS_integrable_ae line 361
28. lemma OAI.TriangularBilliards.reflectedGradS_integrable_ae line 374
29. lemma OAI.TriangularBilliards.directGradS_sub_ae line 389
30. lemma OAI.TriangularBilliards.reflectedGradS_sub_ae line 399
31. lemma OAI.TriangularBilliards.reflectedSmoothingGradient_sub_ae line 410
32. lemma OAI.TriangularBilliards.scaled_gradient_lpNorm_bound line 426
33. lemma OAI.TriangularBilliards.lpNorm_congr_ae_of_strong line 453
34. lemma OAI.TriangularBilliards.scaled_gradient_lpNorm_tendsto_bounded line 460
35. lemma OAI.TriangularBilliards.scaled_gradient_lpNorm_tendsto line 475

    Source documentation

    The small-scaled-derivative estimate for every L² input and the reflected triangular kernel, not merely a dense test class.

    lemma scaled_gradient_lpNorm_tendsto (Q : Triangle) {f : DoublePhase → ℂ}
        (hf : StronglyMeasurable f) (hf₂ : MemLp f 2 (doubleMeasure Q)) :
        Tendsto (fun ε : ℝ => lpNorm (ε • reflectedSmoothingGradient Q ε f) 2 (doubleMeasure Q))
          (𝓝[>] 0) (𝓝 0) := by
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.reflectedSmoothingGradient