AveragedLpPairing.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact averaged kernel pairings with bounded Sobolev densities

theorem OAI.RegularPointCoordinates.kernelAverage_integral_lp line 20
Source documentation
The actual averaged kernel pairing is an L2 heat pairing. This also justifies its initial-time limit without a pointwise kernel limit.
```
theorem kernelAverage_integral_lp {t : ℝ} (ht : 0 < t)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (f : Lp ℝ 2 μ) :
    (∫ z, kernelAverage μ ker t A z * f z ∂μ) =
      ⟪heatAt μ hQ t (uniformDensityLp μ A hA hAt), f⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.heatAt, OAI.RegularPointCoordinates.uniformDensityLp
theorem OAI.RegularPointCoordinates.kernelAverage_integral_lp_intervalIntegrable_zero line 34
Source documentation
The full averaged pairing is integrable down to zero time for L2 densities, including the compact curvature density.
```
theorem kernelAverage_integral_lp_intervalIntegrable_zero
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (f : Lp ℝ 2 μ)
    {T : ℝ} (hT : 0 ≤ T) :
    IntervalIntegrable (fun t => ∫ z, kernelAverage μ ker t A z * f z ∂μ) volume 0 T := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelAverage

theorem OAI.RegularPointCoordinates.kernelAverage_integral_lp_eq_average line 49

Source documentation

The same pairing is the actual average of the heat-evolved density.

theorem kernelAverage_integral_lp_eq_average {t : ℝ} (ht : 0 < t)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (f : Lp ℝ 2 μ) :
    (∫ z, kernelAverage μ ker t A z * f z ∂μ) =
      (μ.real A)⁻¹ * ∫ z in A, heatAt μ hQ t f z ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.heatAt

theorem OAI.RegularPointCoordinates.kernelAverage_mul_lp_integrable line 58
Source documentation
Each positive-time averaged kernel pairing is an ordinary integrable product of two L2 representatives.
```
theorem kernelAverage_mul_lp_integrable {t : ℝ} (ht : 0 < t)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (f : Lp ℝ 2 μ) :
    Integrable (fun z => kernelAverage μ ker t A z * f z) μ := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelAverage
theorem OAI.RegularPointCoordinates.kernel_mul_lp_integrable line 70
Source documentation
The pointwise kernel pairing is also an integrable L2 product.
```
theorem kernel_mul_lp_integrable {t : ℝ} (ht : 0 < t) (x : X) (f : Lp ℝ 2 μ) :
    Integrable (fun z => ker t x z * f z) μ := by
…
```
theorem OAI.RegularPointCoordinates.kernelAverage_difference_integral_lp line 78
Source documentation
Kernel subtraction is valid for these actual integrable products.
```
theorem kernelAverage_difference_integral_lp {t : ℝ} (ht : 0 < t)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (x : X) (f : Lp ℝ 2 μ) :
    (∫ z, (kernelAverage μ ker t A z - ker t x z) * f z ∂μ) =
      ⟪heatAt μ hQ t (uniformDensityLp μ A hA hAt), f⟫_ℝ - kernelHeat μ hQ hk t f x := by
…
```
Mentions: OAI.RegularPointCoordinates.kernelAverage, OAI.RegularPointCoordinates.heatAt, OAI.RegularPointCoordinates.uniformDensityLp, OAI.RegularPointCoordinates.kernelHeat

theorem OAI.RegularPointCoordinates.kernelAverage_difference_lp_intervalIntegrable line 90

Source documentation

All positive-time difference pairings with an L2 density are integrable on compact time intervals.

theorem kernelAverage_difference_lp_intervalIntegrable
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) (x : X) (f : Lp ℝ 2 μ)
    {s t : ℝ} (hs : 0 < s) (hst : s ≤ t) :
    IntervalIntegrable (fun r => ∫ z, (kernelAverage μ ker r A z - ker r x z) * f z ∂μ)
      volume s t := by
…

Mentions: OAI.RegularPointCoordinates.kernelAverage