OAI/Dynamics/TriangleBilliards/SmoothingLimits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.smoothing_lpNorm_tendsto_bounded line 43
2. lemma OAI.TriangularBilliards.smoothing_lpNorm_bound line 76
3. lemma OAI.TriangularBilliards.smoothing_lpNorm_tendsto line 84
4. lemma OAI.TriangularBilliards.Analytic.WeaklyTendsto.inner_right line 134
5. def OAI.TriangularBilliards.smoothingLp line 151
6. lemma OAI.TriangularBilliards.smoothingLp_adjoint line 155
7. lemma OAI.TriangularBilliards.smoothingLp_tendsto line 164
8. lemma OAI.TriangularBilliards.smoothing_variable_pairing line 178
9. lemma OAI.TriangularBilliards.smoothing_toLp_eq line 197
10. lemma OAI.TriangularBilliards.exists_clearance_data line 210

    Source documentation

    One actual long-clearance-segment approximation, with all bounds and its relevant Fourier derivative pairing.

    lemma exists_clearance_data (Q : Triangle) {L ε R T H : ℝ}
        (hε : 0 < ε) (hT : 0 < T) (hH : 0 ≤ H)
        (hR : Q.safetyFactor*ε < R) (hsmall : 2*R*Q.coordinateBound < 1)
        (hL : 2*R+2*ε ≤ L*ε)
        {f : DoubleL2 Q} (hf : ∀ᵐ z ∂doubleMeasure Q, ‖f z‖ ≤ H)
        (hinv : ∀ t, (geodesicHilbertFlow Q).act t f = f)
        (j : ℤ) {U B : DoubleL2 Q}
        (hUB : (geodesicHilbertFlow Q).HasGenerator U B)
        (hB : (angularCircleAction Q).projection (j-1) B = B) :
        ∃ g w p a b : DoubleL2 Q,
          (∀ᵐ z ∂doubleMeasure Q, ‖g z‖ ≤ H) ∧
          ‖g-f‖ ≤ H*(doubleMeasure Q (goodMesh Q L ε T)ᶜ).toReal^(1/2:ℝ) ∧
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.angularCircleAction, OAI.TriangularBilliards.goodMesh

11. lemma OAI.TriangularBilliards.Analytic.weaklyTendsto_of_inner line 271