HeatPoissonAverage.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Time variation of averages for a weak Poisson solution

theorem OAI.RegularPointCoordinates.lp_setAverage_eq_inner line 19

Source documentation

A finite-set average is a continuous linear functional on L².

theorem lp_setAverage_eq_inner (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞)
    (f : Lp ℝ 2 μ) :
    (⨍ x in A, f x ∂μ) =
      (μ.real A)⁻¹ * inner ℝ (indicatorConstLp 2 hA hAt (1:ℝ)) f := by
…

theorem OAI.RegularPointCoordinates.heat_setAverage_continuous line 25
theorem OAI.RegularPointCoordinates.heat_setAverage_add line 30
theorem OAI.RegularPointCoordinates.heat_weakLaplacian_average_hasDerivAt line 38
Source documentation
The weak Laplacian gives the genuine derivative of every finite-set average, including for initial data with no chosen pointwise representative.
```
theorem heat_weakLaplacian_average_hasDerivAt
    (u : SobolevSpace μ hQ) (d : Lp ℝ 2 μ) (hd : IsWeakLaplacian μ hQ u d)
    (A : Set X) (hA : MeasurableSet A) (hAt : μ A ≠ ∞) {t : ℝ} (ht : 0 < t) :
    HasDerivAt (fun s => ⨍ x in A, heatAt μ hQ s (SobolevSpace.toLp μ hQ u) x ∂μ)
      (⨍ x in A, heatAt μ hQ t d x ∂μ) t := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.heatAt, OAI.RegularPointCoordinates.SobolevSpace.toLp