OAI/Dynamics/TriangleBilliards/SecondDerivatives.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.seam_rotationalCR line 38
2. lemma OAI.TriangularBilliards.seam_projected_CR_norms line 60

   Source documentation

   The second spatial jet on the actual smooth seam core. No spectral regularity of an invariant is assumed in this lemma.

   lemma seam_projected_CR_norms {Q : Triangle} {f : DoublePhase → ℂ}
       (hs : SeamCompatible Q f)
       (hd : ∀ v b, ContDiff ℝ ∞ (fun x => f ((x,v),b)))
       {C Cx Cy : ℝ≥0}
       (hC : ∀ x v b, ‖fderiv ℝ (fun y => f ((y,v),b)) x‖ ≤ C)
       (hCx : ∀ x v b, ‖fderiv ℝ (fun y => xDerivative f ((y,v),b)) x‖ ≤ Cx)
       (hCy : ∀ x v b, ‖fderiv ℝ (fun y => yDerivative f ((y,v),b)) x‖ ≤ Cy)
       (hf : MemLp f 2 (doubleMeasure Q))
       (hx : MemLp (xDerivative f) 2 (doubleMeasure Q))
       (hy : MemLp (yDerivative f) 2 (doubleMeasure Q))
       (hxx : MemLp (xDerivative (xDerivative f)) 2 (doubleMeasure Q))
       (hxy : MemLp (xDerivative (yDerivative f)) 2 (doubleMeasure Q))
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DoublePhase, OAI.TriangularBilliards.SeamCompatible, OAI.TriangularBilliards.xDerivative, OAI.TriangularBilliards.yDerivative, OAI.TriangularBilliards.doubleMeasure

3. lemma OAI.TriangularBilliards.Analysis.convolution_uniform_bound line 135
4. lemma OAI.TriangularBilliards.Analysis.convolution_fderiv_eq line 150
5. lemma OAI.TriangularBilliards.Analysis.convolution_second_formula line 159
6. lemma OAI.TriangularBilliards.Analysis.compact_second_bound line 167
7. lemma OAI.TriangularBilliards.Analysis.convolution_second_bound line 177

   Source documentation

   Uniform second jets with an abstract kernel codomain.

   lemma convolution_second_bound (L : E →L[ℝ] F →L[ℝ] G)
       {g : ℂ → F} (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ (f : ℂ → E), Integrable f → ∀ x,
         ‖fderiv ℝ (fderiv ℝ (MeasureTheory.convolution (𝕜 := ℝ) f g L volume)) x‖ ≤ C * (∫ y, ‖f y‖) := by
   …

8. lemma OAI.TriangularBilliards.Analysis.measurable_directional_derivative line 197

   Source documentation

   Joint measurability of a spatial directional derivative requires no angular differentiability or continuity.

   lemma measurable_directional_derivative {A : Type uA} [MeasurableSpace A]
       {f : ℂ × A → ℂ} (hf : Measurable f)
       (hd : ∀ a, Differentiable ℝ (fun x => f (x,a)))
       {v : A → ℂ} (hv : Measurable v) :
       Measurable (fun z : ℂ × A => fderiv ℝ (fun x => f (x,z.2)) z.1 (v z.2)) := by
   …

9. lemma OAI.TriangularBilliards.Analysis.second_bound_comp_constant_derivative line 223
10. lemma OAI.TriangularBilliards.Analysis.norm_second_eq_iterated line 246
11. lemma OAI.TriangularBilliards.Analysis.second_bound_smul line 250
12. lemma OAI.TriangularBilliards.Analysis.second_add line 271
13. lemma OAI.TriangularBilliards.Analysis.second_sum line 282
14. lemma OAI.TriangularBilliards.Analysis.directional_derivative_bound line 292
15. lemma OAI.TriangularBilliards.vertexCutoff_sub_one_compact line 309
16. lemma OAI.TriangularBilliards.vertexCutoff_second_bound line 324
17. lemma OAI.TriangularBilliards.spatialSlice_integral_norm_bound line 334
18. lemma OAI.TriangularBilliards.directS_second_bound line 347
19. lemma OAI.TriangularBilliards.reflectedS_second_bound line 357
20. lemma OAI.TriangularBilliards.reflectedSmoothing_second_bound line 375
21. lemma OAI.TriangularBilliards.supportedSmoothing_second_bound line 394
22. lemma OAI.TriangularBilliards.xDerivative_measurable line 424
23. lemma OAI.TriangularBilliards.yDerivative_measurable line 435
24. lemma OAI.TriangularBilliards.norm_transverseVelocity line 457
25. lemma OAI.TriangularBilliards.xDerivative_fderiv_bound line 461
26. lemma OAI.TriangularBilliards.yDerivative_fderiv_bound line 469
27. lemma OAI.TriangularBilliards.xDerivative_memLp_of_gradient_bound line 477
28. lemma OAI.TriangularBilliards.yDerivative_memLp_of_gradient_bound line 487
29. lemma OAI.TriangularBilliards.seam_projected_CR_norms_of_bounded_jets line 497