PeriodicFastEvaluation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Chain rule for substituting a fast linear phase in a smooth periodic family.

def OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fastValue line 19
lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fastValue_smooth line 22
lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Family.fastValue_fderiv line 27
Source documentation
Both slow and angular terms in the derivative of fast evaluation.
```
lemma fastValue_fderiv (U : Family A E) (ℓ : A →L[ℝ] ℝ) (z : ℝ) (p v : A) :
    fderiv ℝ (U.fastValue ℓ z) p v =
      (U.slow v).val p ((ℓ p / z : ℝ) : Period) +
        (ℓ v / z) • U.angle.val p ((ℓ p / z : ℝ) : Period) := by
…
```
Mentions: OAI.ClosedSurfaceR4.PeriodicExpansion.Family, OAI.ClosedSurfaceR4.PeriodicExpansion.Family.val