OAI/Dynamics/TriangleBilliards/RegularizedModes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.bounded_invariant_regularized_modes line 43

   Source documentation

   The uniform per-coefficient estimate for cutoff regularizations of an actual bounded invariant. The constant depends on the triangle, not the Fourier index, smoothing scale, or the bounded invariant.

   lemma bounded_invariant_regularized_modes (Q : Triangle) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ {H : ℝ} {f : DoublePhase → ℂ}
         (hm : StronglyMeasurable f) (hf : MemLp f 2 (doubleMeasure Q))
         (hH : ∀ z, ‖f z‖ ≤ H)
         (_hfi : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) 0)
         {ε : ℝ} (hε : 0 < ε)
         (_hsmall : 2 * ((Q.safetyFactor + 1) * ε) * Q.coordinateBound < 1) (j : ℤ),
         let w := supportedSmoothing Q ε ((Q.safetyFactor + 1) * ε) f
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.supportedSmoothing

2. lemma OAI.TriangularBilliards.kernel_eq_zero_of_large line 108
3. lemma OAI.TriangularBilliards.fullS_tendsto line 115
4. lemma OAI.TriangularBilliards.directS_eq_full line 136
5. lemma OAI.TriangularBilliards.reflectedS_zero_of_coord_phase line 150
6. lemma OAI.TriangularBilliards.eventually_interior_smoothing line 161
7. lemma OAI.TriangularBilliards.smoothing_pointwise line 182
8. lemma OAI.TriangularBilliards.Triangle.clearance_pos_of_mem_table line 194
9. lemma OAI.TriangularBilliards.supported_smoothing_pointwise line 203
10. lemma OAI.TriangularBilliards.supported_smoothing_lpNorm_tendsto_bounded line 214
11. lemma OAI.TriangularBilliards.directS_integrable_ae line 247
12. lemma OAI.TriangularBilliards.reflectedS_integrable_ae line 258
13. lemma OAI.TriangularBilliards.smoothing_sub_ae line 271
14. lemma OAI.TriangularBilliards.supported_smoothing_sub_ae line 288
15. lemma OAI.TriangularBilliards.supportedSmoothing_norm_le line 296
16. lemma OAI.TriangularBilliards.supportedSmoothing_memLp_of_memLp line 301
17. lemma OAI.TriangularBilliards.supported_smoothing_lpNorm_bound line 308
18. lemma OAI.TriangularBilliards.supported_smoothing_lpNorm_tendsto line 327

    Source documentation

    Strong L2 approximate identity for the actual supported triangular mollifier. No smoothness or invariance is required of the input.

    lemma supported_smoothing_lpNorm_tendsto (Q : Triangle) {K : ℝ} (hK : 0 < K)
        {f : DoublePhase → ℂ} (hf : StronglyMeasurable f) (hf₂ : MemLp f 2 (doubleMeasure Q)) :
        Tendsto (fun ε : ℝ => lpNorm (supportedSmoothing Q ε (K*ε) f - (f : DoublePhase → ℂ)) 2 (doubleMeasure Q))
          (𝓝[>] 0) (𝓝 0) := by
    …

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