L¹ continuity of kernel potentials

An integrable kernel translated by a measurable family of shifts can be integrated against integrable weights. Almost everywhere convergence of the shifts and L¹ convergence of the weights imply L¹ convergence of these potentials. A quantitative estimate separates the weight error from the kernel translation error.

theorem MeasureTheory.Integrable.integrable_prod_comp_sub_mul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [MeasurableSub₂ G] {ν : Measure G} [ν.IsAddRightInvariant] [SFinite ν] {K : Type u_2} [NormedRing K] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] {α : Type u_3} [MeasurableSpace α] {μ : Measure α} {k : G → K} (hk : Integrable k ν) (hmk : Measurable k) {c : α → G} {v : α → K} (hc : AEMeasurable c μ) (hv : Integrable v μ) : Integrable (fun (p : α × G) => k (p.2 - c p.1) * v p.1) (μ.prod ν)

An integrable kernel with integrable weights and a.e.-measurable shifts gives a jointly integrable function (t, z) ↦ k (z - c t) * v t for the product measure.

theorem MeasureTheory.Integrable.integral_comp_sub_mul {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [MeasurableSub₂ G] {ν : Measure G} [ν.IsAddRightInvariant] [SFinite ν] {K : Type u_2} [NormedRing K] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] {α : Type u_3} [MeasurableSpace α] {μ : Measure α} [SFinite μ] {k : G → K} [NormedSpace ℝ K] (hk : Integrable k ν) (hmk : Measurable k) {c : α → G} {v : α → K} (hc : AEMeasurable c μ) (hv : Integrable v μ) : Integrable (fun (z : G) => ∫ (t : α), k (z - c t) * v t ∂μ) ν

An integrable kernel with integrable weights and measurable shifts has an integrable weighted potential after integrating over the shifts.

theorem MeasureTheory.Integrable.integral_norm_kernel_translation_sub_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {ν : Measure G} [ν.IsAddRightInvariant] {K : Type u_2} [NormedAddCommGroup K] {k : G → K} (hk : Integrable k ν) (a b : G) : ∫ (z : G), ‖k (z - a) - k (z - b)‖ ∂ν ≤ 2 * ∫ (z : G), ‖k z‖ ∂ν

The L¹ distance between two translates is at most twice the kernel's L¹ norm.

theorem MeasureTheory.Integrable.integrable_integral_norm_comp_sub_sub_mul_norm {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [MeasurableSub₂ G] {ν : Measure G} [ν.IsAddRightInvariant] [SFinite ν] {K : Type u_2} {V : Type u_3} [NormedAddCommGroup K] [NormedAddCommGroup V] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] {α : Type u_4} [MeasurableSpace α] {μ : Measure α} {k : G → K} (hk : Integrable k ν) (hmk : Measurable k) {a b : α → G} {v : α → V} (ha : AEMeasurable a μ) (hb : AEMeasurable b μ) (hv : Integrable v μ) : Integrable (fun (t : α) => (∫ (z : G), ‖k (z - a t) - k (z - b t)‖ ∂ν) * ‖v t‖) μ

The translation error weighted by an integrable function is integrable.

theorem MeasureTheory.Integrable.tendsto_integral_weighted_kernel_translation_sub {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [MeasurableSub₂ G] {ν : Measure G} [ν.IsAddRightInvariant] [SFinite ν] [IsLocallyFiniteMeasure ν] [ν.InnerRegularCompactLTTop] {K : Type u_2} {V : Type u_3} [NormedAddCommGroup K] [NormedAddCommGroup V] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] {α : Type u_4} [MeasurableSpace α] {μ : Measure α} {k : G → K} (hk : Integrable k ν) (hmk : Measurable k) {cn : ℕ → α → G} {c : α → G} {v : α → V} (hcn : ∀ (n : ℕ), AEMeasurable (cn n) μ) (hc : AEMeasurable c μ) (hv : Integrable v μ) (hlim : ∀ᵐ (t : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => cn n t) Filter.atTop (nhds (c t))) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : α), (∫ (z : G), ‖k (z - cn n t) - k (z - c t)‖ ∂ν) * ‖v t‖ ∂μ) Filter.atTop (nhds 0)

Almost everywhere convergence of shifts gives weighted L¹ translation convergence.

theorem MeasureTheory.Integrable.integral_norm_translated_kernel_mul_sub_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] {ν : Measure G} [ν.IsAddRightInvariant] {K : Type u_2} [NormedRing K] {k : G → K} (hk : Integrable k ν) (a b : G) (u v : K) : ∫ (z : G), ‖k (z - a) * u - k (z - b) * v‖ ∂ν ≤ (∫ (z : G), ‖k z‖ ∂ν) * ‖u - v‖ + (∫ (z : G), ‖k (z - a) - k (z - b)‖ ∂ν) * ‖v‖

For fixed shifts and weights, split the product difference into a weight error and a translation error, retaining the exact L¹ constants.

theorem MeasureTheory.Integrable.integral_norm_kernel_potential_sub_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [MeasurableSub₂ G] {ν : Measure G} [ν.IsAddRightInvariant] [SFinite ν] {K : Type u_2} [NormedRing K] [NormedSpace ℝ K] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] {α : Type u_3} [MeasurableSpace α] {μ : Measure α} [SFinite μ] {k : G → K} (hk : Integrable k ν) (hmk : Measurable k) {a b : α → G} {u v : α → K} (ha : AEMeasurable a μ) (hb : AEMeasurable b μ) (hu : Integrable u μ) (hv : Integrable v μ) : ∫ (z : G), ‖∫ (t : α), k (z - a t) * u t ∂μ - ∫ (t : α), k (z - b t) * v t ∂μ‖ ∂ν ≤ (∫ (z : G), ‖k z‖ ∂ν) * ∫ (t : α), ‖u t - v t‖ ∂μ + ∫ (t : α), (∫ (z : G), ‖k (z - a t) - k (z - b t)‖ ∂ν) * ‖v t‖ ∂μ

A kernel potential difference is bounded by the weight discrepancy and a translation error.

theorem MeasureTheory.Integrable.tendsto_integral_norm_kernel_potential_sub {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [MeasurableSub₂ G] {ν : Measure G} [ν.IsAddRightInvariant] [SFinite ν] [IsLocallyFiniteMeasure ν] [ν.InnerRegularCompactLTTop] {K : Type u_2} [NormedRing K] [NormedSpace ℝ K] [MeasurableSpace K] [BorelSpace K] [SecondCountableTopology K] {α : Type u_4} [MeasurableSpace α] {μ : Measure α} [SFinite μ] {k : G → K} (hk : Integrable k ν) (hmk : Measurable k) {cn : ℕ → α → G} {vn : ℕ → α → K} {c : α → G} {v : α → K} (hcn : ∀ (n : ℕ), AEMeasurable (cn n) μ) (hc : AEMeasurable c μ) (hvn : ∀ (n : ℕ), Integrable (vn n) μ) (hv : Integrable v μ) (hclim : ∀ᵐ (t : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => cn n t) Filter.atTop (nhds (c t))) (hvlim : Filter.Tendsto (fun (n : ℕ) => ∫ (t : α), ‖vn n t - v t‖ ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : G), ‖∫ (t : α), k (z - cn n t) * vn n t ∂μ - ∫ (t : α), k (z - c t) * v t ∂μ‖ ∂ν) Filter.atTop (nhds 0)

Almost everywhere convergence of shifts and L¹ convergence of weights give L¹ convergence of the corresponding kernel potentials.