Backward Potential Pairing

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Heat.backwardHeatPotential_pairing {f ζ : Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.Integrable (fun (q : Parabolic.ParabolicPoint × Parabolic.ParabolicPoint) => backwardHeatKernel q.1 q.2 * ζ q.1 * f q.2) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (v : Parabolic.ParabolicPoint), f v * backwardHeatPotential ζ v = ∫ (z : Parabolic.ParabolicPoint), (∫ (v : Parabolic.ParabolicPoint), backwardHeatKernel z v * f v) * ζ z

theorem CKN.Foundation.Heat.backwardHeatPotential_spatial_pairing {i : Fin 3} {f ζ : Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.Integrable (fun (q : Parabolic.ParabolicPoint × Parabolic.ParabolicPoint) => backwardHeatSpatialKernel i q.1 q.2 * ζ q.1 * f q.2) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (v : Parabolic.ParabolicPoint), f v * backwardHeatPotentialSpatial i ζ v = -∫ (z : Parabolic.ParabolicPoint), (∫ (v : Parabolic.ParabolicPoint), backwardHeatSpatialKernel i z v * f v) * ζ z