AnalyticScalarDerivatives.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Derivatives of the scalar displacement profiles

The one-sided derivatives are glued on the two closed/open half-lines. In particular, the formulas below hold at all four transition points; no transition point is removed from the domain.

theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_if_le_junction line 23
theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_if_le_all line 42
theorem OAI.ThompsonNonamenability.Analytic.if_lt_eq_if_le line 62
theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_a_middle line 70
theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_theta_middle line 76
theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_a line 83
Source documentation
The radial scalar profile is differentiable at every real point, including its two junctions.
```
theorem hasDerivAt_a (t : ℝ) : HasDerivAt a (aDeriv t) t := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.a, OAI.ThompsonNonamenability.Analytic.aDeriv
theorem OAI.ThompsonNonamenability.Analytic.hasDerivAt_theta line 115
Source documentation
The angular scalar profile is differentiable at every real point, including its two junctions.
```
theorem hasDerivAt_theta (t : ℝ) : HasDerivAt theta (thetaDeriv t) t := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.theta, OAI.ThompsonNonamenability.Analytic.thetaDeriv
theorem OAI.ThompsonNonamenability.Analytic.deriv_a line 146
theorem OAI.ThompsonNonamenability.Analytic.deriv_theta line 148
theorem OAI.ThompsonNonamenability.Analytic.differentiable_a line 150
theorem OAI.ThompsonNonamenability.Analytic.differentiable_theta line 152
theorem OAI.ThompsonNonamenability.Analytic.continuous_a line 155
theorem OAI.ThompsonNonamenability.Analytic.continuous_theta line 157
theorem OAI.ThompsonNonamenability.Analytic.continuous_aDeriv line 159
theorem OAI.ThompsonNonamenability.Analytic.continuous_thetaDeriv line 161