OAI/Dynamics/TriangleBilliards/ClearanceAverages.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularBilliards.clearanceAverage line 41
2. lemma OAI.TriangularBilliards.clearanceAverage_bounded line 45
3. lemma OAI.TriangularBilliards.clearanceAverage_zero line 57
4. lemma OAI.TriangularBilliards.clearanceAverage_estimates line 77
5. lemma OAI.TriangularBilliards.restricted_clearance_zero_time line 101
6. lemma OAI.TriangularBilliards.clearanceAverage_generator_supported line 120
7. lemma OAI.TriangularBilliards.exists_bounded_supported_representative line 153

   Source documentation

   Choose a genuinely measurable everywhere bounded, spatially supported representative; no pointwise assertion about an arbitrary Lp representative is used.

   lemma exists_bounded_supported_representative (Q : Triangle) {u : DoubleL2 Q} {H A : ℝ}
       (hH : 0 ≤ H) (hu : ∀ᵐ z ∂doubleMeasure Q, ‖u z‖ ≤ H)
       (hs : ∀ᵐ z ∂doubleMeasure Q, z ∈ unsafeSet Q A → u z = 0) :
       ∃ f : DoublePhase → ℂ, StronglyMeasurable f ∧
         (∀ z, ‖f z‖ ≤ H) ∧ SpatiallyZero Q A f ∧ f =ᵐ[doubleMeasure Q] u := by
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.unsafeSet, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.SpatiallyZero

8. lemma OAI.TriangularBilliards.doubleL2_norm_le_of_ae_bound line 182
9. lemma OAI.TriangularBilliards.reflectedSmoothingY_norm_bound line 186
10. lemma OAI.TriangularBilliards.scaled_smoothingY_norm_tendsto line 193
11. lemma OAI.TriangularBilliards.badMesh_real_bound line 215
12. lemma OAI.TriangularBilliards.supported_source_CR line 246

    Source documentation

    Quantitative global energy for a supported mollifier with a nonzero transport source. All graphs are the actual specular generators.

    lemma supported_source_CR (Q : Triangle) {ε R A T H : ℝ}
        (hε : 0 < ε) (hT : 0 < T) (hH : 0 ≤ H)
        (hR : Q.safetyFactor*ε < R) (hsmall : 2*R*Q.coordinateBound < 1)
        (hA : 2*R+2*ε ≤ A)
        {f p : DoublePhase → ℂ} (hfm : StronglyMeasurable f) (hpm : StronglyMeasurable p)
        (hf : MemLp f 2 (doubleMeasure Q)) (hp : MemLp p 2 (doubleMeasure Q))
        (hfp : (geodesicHilbertFlow Q).HasGenerator (hf.toLp f) (hp.toLp p))
        (hfb : ∀ z, ‖f z‖ ≤ H) (hpb : ∀ z, ‖p z‖ ≤ 2*H/T)
        (hfs : SpatiallyZero Q A f) (hps : SpatiallyZero Q A p) (j : ℤ)
        {U B : DoubleL2 Q} (hUB : (geodesicHilbertFlow Q).HasGenerator U B)
        (hB : (angularCircleAction Q).projection (j-1) B = B) :
        let hw := supportedSmoothing_memLp Q hε R hfm hfb
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.doubleMeasure, OAI.TriangularBilliards.geodesicHilbertFlow, OAI.TriangularBilliards.SpatiallyZero, OAI.TriangularBilliards.DoubleL2, OAI.TriangularBilliards.angularCircleAction, OAI.TriangularBilliards.supportedSmoothing_memLp