PeriodicIntegralOperator.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded linear operators underlying normalized periodic integration.

lemma OAI.ClosedSurfaceR4.PeriodicIntegralOperator.continuous_lift line 20
def OAI.ClosedSurfaceR4.PeriodicIntegralOperator.rawIntegral line 26
Source documentation
Integration from zero to a fixed real time is bounded on the space of continuous periodic functions, even when that time is outside one period.
```
def rawIntegral (x : ℝ) : C(Period, E) →L[ℝ] E :=
…
```
lemma OAI.ClosedSurfaceR4.PeriodicIntegralOperator.rawIntegral_apply line 40
lemma OAI.ClosedSurfaceR4.PeriodicIntegralOperator.rawIntegral_continuous line 43
lemma OAI.ClosedSurfaceR4.PeriodicIntegralOperator.rawIntegral_norm_unit line 48
def OAI.ClosedSurfaceR4.PeriodicIntegralOperator.primitiveMean line 57
Source documentation
The mean of the unnormalized primitive is also a bounded linear map.
```
def primitiveMean : C(Period, E) →L[ℝ] E :=
…
```
def OAI.ClosedSurfaceR4.PeriodicIntegralOperator.normalizedIntegral line 78
Source documentation
The normalized primitive at a fixed time, with its linear dependence on all periodic input data made explicit.
```
def normalizedIntegral (x : ℝ) : C(Period, E) →L[ℝ] E :=
…
```
lemma OAI.ClosedSurfaceR4.PeriodicIntegralOperator.normalizedIntegral_apply line 81
lemma OAI.ClosedSurfaceR4.PeriodicIntegralOperator.normalizedIntegral_norm_unit line 84
theorem OAI.ClosedSurfaceR4.PeriodicIntegralOperator.contDiff_normalizedIntegral line 102
Source documentation
Smooth dependence on an external parameter follows from the proved bounded linear operator, with no parameter-differentiation assumption.
```
theorem contDiff_normalizedIntegral {F : P → C(Period, E)}
    (hF : ContDiff ℝ ∞ F) (x : ℝ) :
    ContDiff ℝ ∞ (fun p => normalizedIntegral x (F p)) :=
…
```
Mentions: OAI.ClosedSurfaceR4.PeriodicIntegralOperator.normalizedIntegral
theorem OAI.ClosedSurfaceR4.PeriodicIntegralOperator.normalizedIntegral_fderiv line 107