PlaneHeatOperator.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The normalized Gaussian and its first spatial derivatives act on every finite jet space.

def OAI.ForcedComputation.PlaneHeat.heatOperator line 17
Source documentation
The Gaussian heat operator on bounded spatial jets of order k.
```
def heatOperator (k : ℕ) (t : ℝ) (ht : 0 < t) :
    BoundedSpatialJets.Space Plane F k →L[ℝ] BoundedSpatialJets.Space Plane F k :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
def OAI.ForcedComputation.PlaneHeat.gradientOperator line 22
Source documentation
Convolution by one Cartesian derivative of the Gaussian.
```
def gradientOperator (k : ℕ) (t : ℝ) (ht : 0 < t) (j : Fin 2) :
    BoundedSpatialJets.Space Plane F k →L[ℝ] BoundedSpatialJets.Space Plane F k :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space
theorem OAI.ForcedComputation.PlaneHeat.norm_heatOperator_le line 27
theorem OAI.ForcedComputation.PlaneHeat.norm_gradientOperator_le line 37
theorem OAI.ForcedComputation.PlaneHeat.heatOperator_apply line 44
Source documentation
The zeroth component is the usual pointwise Gaussian convolution.
```
theorem heatOperator_apply (k : ℕ) (t : ℝ) (ht : 0 < t)
    (J : BoundedSpatialJets.Space Plane F k) (x : Plane) :
    BoundedSpatialJets.function Plane F k (heatOperator F k t ht J) x =
      ∫ y, kernel t y • BoundedSpatialJets.function Plane F k J (x - y) :=
…
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.PlaneHeat.heatOperator, OAI.ForcedComputation.PlaneHeat.kernel
theorem OAI.ForcedComputation.PlaneHeat.gradientOperator_apply line 51
theorem OAI.ForcedComputation.PlaneHeat.heatOperator_jet line 59
Source documentation
Every supplied derivative is transported by the same Gaussian kernel.
```
theorem heatOperator_jet (k : ℕ) (t : ℝ) (ht : 0 < t)
    (J : BoundedSpatialJets.Space Plane F k) (i : Fin (k + 1)) (x : Plane) :
    (heatOperator F k t ht J).val i x = ∫ y, kernel t y • J.val i (x - y) := rfl
```
Mentions: OAI.ForcedComputation.BoundedSpatialJets.Space, OAI.ForcedComputation.PlaneHeat.heatOperator, OAI.ForcedComputation.PlaneHeat.kernel
theorem OAI.ForcedComputation.PlaneHeat.gradientOperator_jet line 63
theorem OAI.ForcedComputation.PlaneHeat.norm_heatOperator_apply_le line 68
theorem OAI.ForcedComputation.PlaneHeat.norm_gradientOperator_apply_le line 75