EulerRigidity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Rigidity of the Euler equation on a ball

The Euclidean limit in the sharp projection argument satisfies an Euler equation with affine forcing. Two derivatives suffice to force the limit to be affine; harmonic analyticity is not needed for this step.

theorem OAI.RegularPointCoordinates.eq_zero_of_continuousAt_eq_on_Ioo line 23
Source documentation
A continuous function constant immediately to the right has the same value at the endpoint.
```
theorem eq_zero_of_continuousAt_eq_on_Ioo {g : ℝ → ℝ} {c R : ℝ}
    (hR : 0 < R) (hg : ContinuousAt g 0)
    (heq : ∀ t ∈ Ioo 0 R, g t = c) : g 0 = c := by
…
```

theorem OAI.RegularPointCoordinates.scalar_euler_derivative line 33

Source documentation

Differentiating the scalar Euler equation cancels the first derivatives.

theorem scalar_euler_derivative {f f' f'' : ℝ → ℝ} {ell k R t : ℝ}
    (ht : t ∈ Ioo (-R) R)
    (hf : HasDerivAt f (f' t) t) (hf' : HasDerivAt f' (f'' t) t)
    (heuler : ∀ s ∈ Ioo (-R) R, s * f' s = f s + ell * s + k) :
    t * f'' t = ell := by
…

theorem OAI.RegularPointCoordinates.scalar_euler_ray_affine line 50

Source documentation

A twice differentiable scalar ray satisfying the affine-forced Euler equation has zero linear forcing and the affine value at time one.

theorem scalar_euler_ray_affine {f f' f'' : ℝ → ℝ} {ell k R : ℝ}
    (hR : 1 < R)
    (hf : ∀ t ∈ Ioo (-R) R, HasDerivAt f (f' t) t)
    (hf' : ∀ t ∈ Ioo (-R) R, HasDerivAt f' (f'' t) t)
    (heuler : ∀ t ∈ Ioo (-R) R, t * f' t = f t + ell * t + k) :
    ell = 0 ∧ k = -f 0 ∧ f 1 = f 0 + f' 0 := by
…

theorem OAI.RegularPointCoordinates.euler_linear_forcing_eq_zero line 104

Source documentation

At the origin, differentiating the Euler equation forces its linear forcing to vanish. The derivative of the radial factor cancels Dw 0.

theorem euler_linear_forcing_eq_zero {w : E → ℝ}
    {Dw : E → E →L[ℝ] ℝ} {DDw : E →L[ℝ] (E →L[ℝ] ℝ)}
    {ell : E →L[ℝ] ℝ} {k R : ℝ} (hR : 0 < R)
    (hw : HasFDerivAt w (Dw 0) 0) (hDw : HasFDerivAt Dw DDw 0)
    (heuler : ∀ x ∈ Metric.ball 0 R, Dw x x = w x + ell x + k) :
    ell = 0 := by
…

theorem OAI.RegularPointCoordinates.euler_rigidity_of_hasFDerivAt line 124

Source documentation

The affine conclusion on a ball, with the two derivative fields explicit. No continuity of the second derivative is required.

theorem euler_rigidity_of_hasFDerivAt {w : E → ℝ}
    {Dw : E → E →L[ℝ] ℝ} {DDw : E → E →L[ℝ] (E →L[ℝ] ℝ)}
    {ell : E →L[ℝ] ℝ} {k R : ℝ} (hR : 0 < R)
    (hw : ∀ x ∈ Metric.ball 0 R, HasFDerivAt w (Dw x) x)
    (hDw : ∀ x ∈ Metric.ball 0 R, HasFDerivAt Dw (DDw x) x)
    (heuler : ∀ x ∈ Metric.ball 0 R, Dw x x = w x + ell x + k) :
    ell = 0 ∧ k = -w 0 ∧ ∀ x ∈ Metric.ball 0 R, w x = w 0 + Dw 0 x := by
…

theorem OAI.RegularPointCoordinates.euler_rigidity_of_contDiffOn line 170

Source documentation

C² version of the Euler rigidity theorem used for the smooth Euclidean limit in pi:limiting-euler-equation.

theorem euler_rigidity_of_contDiffOn {w : E → ℝ} {ell : E →L[ℝ] ℝ} {k R : ℝ}
    (hR : 0 < R) (hw : ContDiffOn ℝ 2 w (Metric.ball 0 R))
    (heuler : ∀ x ∈ Metric.ball 0 R,
      fderiv ℝ w x x = w x + ell x + k) :
    ell = 0 ∧ k = -w 0 ∧
      ∀ x ∈ Metric.ball 0 R, w x = w 0 + fderiv ℝ w 0 x := by
…