ProcessorFlowSmooth.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Smooth dependence for an arbitrary smooth periodic processor input. The compact-detector input is not restricted to finite Hamiltonian expressions.

theorem OAI.ForcedComputation.periodic_joint_bound line 17
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput.derivative_time_periodic line 35
Source documentation
Time periodicity passes to the total space-time derivative.
```
theorem derivative_time_periodic {V : ℝ → Plane → Plane} (hV : ProcessorInput V)
    (x : Plane) : Function.Periodic (fun t => fderiv ℝ (Function.uncurry V) (t,x)) 1 := by
…
```
Mentions: OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput.joint_derivative_bound line 46
Source documentation
Smooth periodicity supplies the qualitative joint derivative bound needed for the flow.
```
theorem joint_derivative_bound {V : ℝ → Plane → Plane} (hV : ProcessorInput V) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ p, ‖fderiv ℝ (Function.uncurry V) p‖ ≤ C := by
…
```
Mentions: OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput.joint_lipschitz line 54
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput.transition_joint_smooth line 62
Source documentation
Every actual transition of the supplied processor is jointly smooth.
```
theorem transition_joint_smooth {V : ℝ → Plane → Plane} (hV : ProcessorInput V)
    {Ψ : ℝ → ℝ → Plane → Plane} (hΨ : IsPlanarTransition V Ψ) :
    ContDiff ℝ ∞ (fun p : ℝ × (ℝ × Plane) => Ψ p.1 p.2.1 p.2.2) := by
…
```
Mentions: OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput, OAI.ForcedComputation.IsPlanarTransition
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput.variations line 70
Source documentation
The first and second variational equations are consequences of the input data.
```
theorem variations {V : ℝ → Plane → Plane} (hV : ProcessorInput V)
    {Ψ : ℝ → ℝ → Plane → Plane} (hΨ : IsPlanarTransition V Ψ) : PlanarVariations V Ψ :=
…
```
Mentions: OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput, OAI.ForcedComputation.IsPlanarTransition, OAI.ForcedComputation.PlanarVariations
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput.backward_smooth line 75
Source documentation
The backward map used by the detector has the same joint smoothness.
```
theorem backward_smooth {V : ℝ → Plane → Plane} (hV : ProcessorInput V)
    {Ψ : ℝ → ℝ → Plane → Plane} (hΨ : IsPlanarTransition V Ψ) :
    ContDiff ℝ ∞ (fun p : ℝ × Plane => Ψ p.1 (-p.1) p.2) :=
…
```
Mentions: OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput, OAI.ForcedComputation.IsPlanarTransition