OAI/Dynamics/TriangleBilliards/KernelBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularBilliards.Analytic.sqrt_sq line 24
2. lemma OAI.TriangularBilliards.Analytic.lintegral_sq_le_mass line 29

   Source documentation

   Cauchy–Schwarz against the constant one, including infinite measures.

   lemma lintegral_sq_le_mass {α : Type uAlpha} [MeasurableSpace α]
       (μ : Measure α) {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
       (∫⁻ x, f x ∂μ) ^ (2 : ℕ) ≤ (∫⁻ x, f x ^ (2 : ℕ) ∂μ) * μ univ := by
   …

3. lemma OAI.TriangularBilliards.Analytic.lintegral_kernel_sq line 46

   Source documentation

   Weighted Cauchy–Schwarz in a form that does not need integrability assumptions: any infinite expressions remain in ℝ≥0∞.

   lemma lintegral_kernel_sq {α : Type uAlpha} [MeasurableSpace α]
       (μ : Measure α) {k f : α → ℝ≥0∞} (hk : AEMeasurable k μ)
       (hf : AEMeasurable f μ) :
       (∫⁻ x, k x * f x ∂μ) ^ (2 : ℕ) ≤
         (∫⁻ x, k x ∂μ) * (∫⁻ x, k x * f x ^ (2 : ℕ) ∂μ) := by
   …

4. lemma OAI.TriangularBilliards.Analytic.kernel_schur_sq line 60

   Source documentation

   Schur's L² bound. Bounds for the absolute kernel integral in each variable control the squared L² seminorm of its positive majorant.

   lemma kernel_schur_sq {α : Type uAlpha} {β : Type uBeta} [MeasurableSpace α] [MeasurableSpace β]
       (μ : Measure α) (ν : Measure β) [SFinite μ] [SFinite ν]
       {K : α → β → ℝ≥0∞} (hK : Measurable (Function.uncurry K))
       {f : β → ℝ≥0∞} (hf : Measurable f) {A B : ℝ≥0∞}
       (hrow : ∀ x, ∫⁻ y, K x y ∂ν ≤ A)
       (hcol : ∀ y, ∫⁻ x, K x y ∂μ ≤ B) :
       ∫⁻ x, (∫⁻ y, K x y * f y ∂ν) ^ (2 : ℕ) ∂μ ≤
         A * B * ∫⁻ y, f y ^ (2 : ℕ) ∂ν := by
   …

5. lemma OAI.TriangularBilliards.Analytic.kernel_integral_schur_sq line 94

   Source documentation

   The Schur bound for a vector-valued integral with a scalar kernel majorant. It also covers norm-preserving parallel transports between fibers.

   lemma kernel_integral_schur_sq {α : Type uAlpha} {β : Type uBeta} {E : Type uE}
       [MeasurableSpace α] [MeasurableSpace β]
       [NormedAddCommGroup E] [NormedSpace ℝ E]
       (μ : Measure α) (ν : Measure β) [SFinite μ] [SFinite ν]
       {K : α → β → ℝ≥0∞} (hK : Measurable (Function.uncurry K))
       {f : β → ℝ≥0∞} (hf : Measurable f) {A B : ℝ≥0∞}
       (hrow : ∀ x, ∫⁻ y, K x y ∂ν ≤ A)
       (hcol : ∀ y, ∫⁻ x, K x y ∂μ ≤ B)
       {F : α → β → E} (hF : ∀ x y, ‖F x y‖ₑ ≤ K x y * f y) :
       ∫⁻ x, ‖∫ y, F x y ∂ν‖ₑ ^ (2 : ℕ) ∂μ ≤
         A * B * ∫⁻ y, f y ^ (2 : ℕ) ∂ν := by
   …

6. lemma OAI.TriangularBilliards.Analytic.fiber_kernel_integral_schur_sq line 115

   Source documentation

   Fiberwise Schur with the genuine product measure. The kernel acts only on the spatial variable, while the additional fiber variable is kept parallel. A measure-preserving fiber substitution can subsequently be used for unfolded reflected terms.

   lemma fiber_kernel_integral_schur_sq {α : Type uAlpha} {β : Type uBeta} {γ : Type uGamma} {E : Type uE}
       [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
       [NormedAddCommGroup E] [NormedSpace ℝ E]
       (μ : Measure α) (ν : Measure β) (σ : Measure γ)
       [SFinite μ] [SFinite ν] [SFinite σ]
       {K : α → β → ℝ≥0∞} (hK : Measurable (Function.uncurry K))
       {f : β × γ → ℝ≥0∞} (hf : Measurable f) {A B : ℝ≥0∞}
       (hrow : ∀ x, ∫⁻ y, K x y ∂ν ≤ A)
       (hcol : ∀ y, ∫⁻ x, K x y ∂μ ≤ B)
       {F : (α × γ) → β → E} (hFm : StronglyMeasurable (Function.uncurry F))
       (hF : ∀ x c y, ‖F (x, c) y‖ₑ ≤ K x y * f (y, c)) :
       ∫⁻ p, ‖∫ y, F p y ∂ν‖ₑ ^ (2 : ℕ) ∂μ.prod σ ≤
   …

7. lemma OAI.TriangularBilliards.Analytic.memLp_kernel_integral line 143

   Source documentation

   In particular, genuine strongly measurable kernel integrals map L² to L² whenever both Schur constants are finite.

   lemma memLp_kernel_integral {α : Type uAlpha} {β : Type uBeta} {E : Type uE} {G : Type uG}
       [MeasurableSpace α] [MeasurableSpace β]
       [NormedAddCommGroup E] [NormedSpace ℝ E]
       [NormedAddCommGroup G]
       (μ : Measure α) (ν : Measure β) [SFinite μ] [SFinite ν]
       {K : α → β → ℝ≥0∞} (hK : Measurable (Function.uncurry K))
       {f : β → G} (hf : StronglyMeasurable f) (hf₂ : MemLp f 2 ν)
       {A B : ℝ≥0∞} (hA : A ≠ ⊤) (hB : B ≠ ⊤)
       (hrow : ∀ x, ∫⁻ y, K x y ∂ν ≤ A)
       (hcol : ∀ y, ∫⁻ x, K x y ∂μ ≤ B)
       {F : α → β → E} (hFm : StronglyMeasurable (Function.uncurry F))
       (hF : ∀ x y, ‖F x y‖ₑ ≤ K x y * ‖f y‖ₑ) :
   …

8. lemma OAI.TriangularBilliards.Analytic.integrable_kernel_ae line 169

   Source documentation

   The row integrals used above genuinely exist almost everywhere; the preceding L² estimate is not exploiting the default value of an undefined Bochner integral.

   lemma integrable_kernel_ae {α : Type uAlpha} {β : Type uBeta} {E : Type uE} {G : Type uG}
       [MeasurableSpace α] [MeasurableSpace β]
       [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G]
       (μ : Measure α) (ν : Measure β) [SFinite μ] [SFinite ν]
       {K : α → β → ℝ≥0∞} (hK : Measurable (Function.uncurry K))
       {f : β → G} (hf : StronglyMeasurable f) (hf₂ : MemLp f 2 ν)
       {A B : ℝ≥0∞} (hA : A ≠ ⊤) (hB : B ≠ ⊤)
       (hrow : ∀ x, ∫⁻ y, K x y ∂ν ≤ A)
       (hcol : ∀ y, ∫⁻ x, K x y ∂μ ≤ B)
       {F : α → β → E} (hFm : StronglyMeasurable (Function.uncurry F))
       (hF : ∀ x y, ‖F x y‖ₑ ≤ K x y * ‖f y‖ₑ) :
       ∀ᵐ x ∂μ, Integrable (F x) ν := by
   …