OAI/Dynamics/TriangleBilliards/KernelAdjoints.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.Analysis.real_kernel_adjoint_slice line 31

   Source documentation

   Fubini for a real bounded spatial kernel. Both input slices are merely integrable; neither is differentiated.

   lemma real_kernel_adjoint_slice {A : Type uA} [MeasurableSpace A]
       {μ : Measure A} [SFinite μ] {k l : A → A → ℝ}
       (hk : StronglyMeasurable (Function.uncurry k)) {K : ℝ}
       (hK : ∀ x y, |k x y| ≤ K) (hs : ∀ x y, k x y = l y x)
       {f g : A → ℂ} (hf : Integrable f μ) (hg : Integrable g μ) :
       (∫ x, (∫ y, k x y • f y ∂μ) * conj (g x) ∂μ) =
         ∫ y, f y * conj (∫ x, l y x • g x ∂μ) ∂μ := by
   …

2. def OAI.TriangularBilliards.Analysis.fiberKernel line 67
3. lemma OAI.TriangularBilliards.Analysis.fiberKernel_adjoint line 74

   Source documentation

   The transport-reversing kernel identity gives the adjoint on a product space. This is applicable to both the direct term (J = id) and a wall reflection, including a derivative kernel with the opposite sign.

   lemma fiberKernel_adjoint {A : Type uA} {C : Type uC} [MeasurableSpace A] [MeasurableSpace C]
       {μ : Measure A} {ν : Measure C} [SFinite μ] [SFinite ν]
       {J : C → C} (hJ : MeasurePreserving J ν ν) (hJe : MeasurableEmbedding J)
       (hJJ : Function.Involutive J) {k l : A → A → C → ℝ}
       (hk : ∀ c, StronglyMeasurable (Function.uncurry (fun x y => k x y c)))
       (hK : ∀ c, ∃ K : ℝ, ∀ x y, |k x y c| ≤ K)
       (hs : ∀ x y c, k x y c = l y x (J c))
       {f g : A × C → ℂ} (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν))
       (hpair₁ : Integrable (fun z => fiberKernel μ J k f z * conj (g z)) (μ.prod ν))
       (hpair₂ : Integrable (fun z => f z * conj (fiberKernel μ J l g z)) (μ.prod ν)) :
       (∫ z, fiberKernel μ J k f z * conj (g z) ∂μ.prod ν) =
         ∫ z, f z * conj (fiberKernel μ J l g z) ∂μ.prod ν := by
   …

   Mentions: OAI.TriangularBilliards.Analysis.fiberKernel

4. lemma OAI.TriangularBilliards.kernel_swap line 102
5. lemma OAI.TriangularBilliards.kernel_wall_swap line 105
6. lemma OAI.TriangularBilliards.kernel_fderiv_neg line 109
7. lemma OAI.TriangularBilliards.kernel_derivative_swap line 113
8. lemma OAI.TriangularBilliards.kernel_wall_derivative_swap line 120

   Source documentation

   Reversal of a reflected short segment also reverses its transported kernel derivative. This is proved from the actual wall unfolding.

   lemma kernel_wall_derivative_swap (Q : Triangle) (i : Fin 3) (ε : ℝ) (x y V : ℂ) :
       fderiv ℝ (kernel ε) (x-wallReflection Q i y) V =
         -fderiv ℝ (kernel ε) (y-wallReflection Q i x) (reflect (Q.tangent i) V) := by
   …

   Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.wallReflection, OAI.TriangularBilliards.reflect

9. lemma OAI.TriangularBilliards.Analysis.fiberKernel_stronglyMeasurable line 144
10. lemma OAI.TriangularBilliards.Analysis.fiberKernel_memLp line 152
11. lemma OAI.TriangularBilliards.Analysis.memLp_conj line 183
12. lemma OAI.TriangularBilliards.Analysis.fiberKernel_L2_adjoint line 188
13. abbrev OAI.TriangularBilliards.DirectionParity line 212
14. def OAI.TriangularBilliards.associatedField line 214
15. lemma OAI.TriangularBilliards.associatedField_memLp line 217
16. lemma OAI.TriangularBilliards.associatedField_stronglyMeasurable line 230
17. lemma OAI.TriangularBilliards.double_integral_assoc line 234
18. def OAI.TriangularBilliards.directionParityReflection line 244
19. lemma OAI.TriangularBilliards.directionParityReflection_involutive line 247
20. lemma OAI.TriangularBilliards.measurePreserving_directionParity line 254
21. lemma OAI.TriangularBilliards.measurableEmbedding_directionParity line 261
22. def OAI.TriangularBilliards.doubleKernel line 269

    Source documentation

    Kernel integration on the two physical triangle copies, with the exact unnormalized Euclidean spatial integral and normalized phase pairing.

    def doubleKernel (Q : Triangle) (J : DirectionParity → DirectionParity)
        (k : ℂ → ℂ → DirectionParity → ℝ) (f : DoublePhase → ℂ)
        (z : DoublePhase) : ℂ :=
    …

    Mentions: OAI.TriangularBilliards.Triangle, OAI.TriangularBilliards.DirectionParity, OAI.TriangularBilliards.DoublePhase

23. lemma OAI.TriangularBilliards.doubleKernel_adjoint line 275
24. lemma OAI.TriangularBilliards.doubleKernel_neg line 294
25. lemma OAI.TriangularBilliards.doubleKernel_skew line 299