HomogeneousDatum.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

The prescribed homogeneous axisymmetric datum

The field StationaryNS.homogeneousDatum is the datum V(130z / (r² + z²)) from the homogeneous-datum subsection of Stationary instability and nonuniqueness for axisymmetric swirl-free Navier–Stokes. It is homogeneous of degree -1, axisymmetric and swirl-free, smooth and classically solenoidal away from the origin, and square integrable on every compact set.

abbrev OAI.StationaryNS.Space line 31
abbrev OAI.StationaryNS.Field line 32
def OAI.StationaryNS.radiusSq line 35
Source documentation
The square of the distance to the origin, in Cartesian coordinates.
```
def radiusSq (x : Space) : ℝ := x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2
```
Mentions: OAI.StationaryNS.Space
def OAI.StationaryNS.homogeneousDatum line 40
Source documentation
The homogeneous datum V(130z/(r²+z²)) of sa:homogeneous-datum, written in Cartesian coordinates. Its value at the origin is fixed to zero; that value has no bearing on its distributional interpretation.
```
def homogeneousDatum (x : Space) : Space :=
…
```
Mentions: OAI.StationaryNS.Space
theorem OAI.StationaryNS.radiusSq_ne_zero line 46
theorem OAI.StationaryNS.radiusSq_smul line 56
theorem OAI.StationaryNS.homogeneousDatum_zero line 60
theorem OAI.StationaryNS.homogeneousDatum_smul line 65
Source documentation
Homogeneity of degree -1, with every nonzero real scale allowed.
```
theorem homogeneousDatum_smul {t : ℝ} (ht : t ≠ 0) (x : Space) :
    homogeneousDatum (t • x) = t⁻¹ • homogeneousDatum x := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum
def OAI.StationaryNS.reflectZ line 77
Source documentation
Reflection in the horizontal plane.
```
def reflectZ (x : Space) : Space := WithLp.toLp 2 ![x 0, x 1, -x 2]
```
Mentions: OAI.StationaryNS.Space
theorem OAI.StationaryNS.radiusSq_reflectZ line 79
theorem OAI.StationaryNS.homogeneousDatum_parity line 83
Source documentation
Positive vector reflection parity of the prescribed homogeneous datum.
```
theorem homogeneousDatum_parity (x : Space) :
    homogeneousDatum (reflectZ x) = reflectZ (homogeneousDatum x) := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum, OAI.StationaryNS.reflectZ
theorem OAI.StationaryNS.homogeneousDatum_swirlFree line 90
Source documentation
The Cartesian angular component is zero.
```
theorem homogeneousDatum_swirlFree (x : Space) :
    x 0 * homogeneousDatum x 1 - x 1 * homogeneousDatum x 0 = 0 := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum
theorem OAI.StationaryNS.homogeneousDatum_contDiffOn line 96
Source documentation
The datum is smooth away from its singular point.
```
theorem homogeneousDatum_contDiffOn :
    ContDiffOn ℝ ⊤ homogeneousDatum ({0}ᶜ : Set Space) := by
…
```
Mentions: OAI.StationaryNS.homogeneousDatum, OAI.StationaryNS.Space
def OAI.StationaryNS.drift line 111
Source documentation
The classical radial drift x·∇u.
```
def drift (u : Field) (x : Space) : Space := fderiv ℝ u x x
```
Mentions: OAI.StationaryNS.Field, OAI.StationaryNS.Space
theorem OAI.StationaryNS.homogeneousDatum_euler line 114
Source documentation
Euler's identity for the prescribed degree -1 datum.
```
theorem homogeneousDatum_euler {x : Space} (hx : x ≠ 0) :
    drift homogeneousDatum x + homogeneousDatum x = 0 := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.drift, OAI.StationaryNS.homogeneousDatum
def OAI.StationaryNS.divergence line 140
Source documentation
Cartesian divergence at points where the field is differentiable.
```
def divergence (u : Field) (x : Space) : ℝ :=
…
```
Mentions: OAI.StationaryNS.Field, OAI.StationaryNS.Space
theorem OAI.StationaryNS.homogeneousDatum_divergence line 145
Source documentation
The datum is classically solenoidal off the origin. Distributional solenoidality across the singular point needs a separate small-sphere estimate.
```
theorem homogeneousDatum_divergence {x : Space} (hx : x ≠ 0) :
    divergence homogeneousDatum x = 0 := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.divergence, OAI.StationaryNS.homogeneousDatum
def OAI.StationaryNS.axialUnit line 167
Source documentation
Unit vector along the axis of symmetry.
```
def axialUnit : Space := EuclideanSpace.single 2 1
```
Mentions: OAI.StationaryNS.Space
def OAI.StationaryNS.AxisymmetricSwirlFree line 172
Source documentation
Invariance under the full orthogonal group fixing the vertical axis pointwise. Unlike invariance under rotations alone, this includes reflections in vertical planes and excludes a swirl component.
```
def AxisymmetricSwirlFree (u : Field) : Prop :=
…
```
Mentions: OAI.StationaryNS.Field
theorem OAI.StationaryNS.radiusSq_eq_normSq line 175
theorem OAI.StationaryNS.homogeneousDatum_vector line 179
Source documentation
A coordinate-free expression useful for the orthogonal symmetries.
```
theorem homogeneousDatum_vector (x : Space) :
    homogeneousDatum x = (130 / radiusSq x ^ 2) •
      ((radiusSq x - 2 * x 2 ^ 2) • x - (radiusSq x * x 2) • axialUnit) := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum, OAI.StationaryNS.radiusSq, OAI.StationaryNS.axialUnit
theorem OAI.StationaryNS.homogeneousDatum_axisymmetricSwirlFree line 185
theorem OAI.StationaryNS.homogeneousDatum_norm line 198
Source documentation
The singular datum obeys the pointwise inverse-distance bound, interpreted with Lean's zero inverse at the origin.
```
theorem homogeneousDatum_norm (x : Space) : ‖homogeneousDatum x‖ ≤ 260 / ‖x‖ := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum
theorem OAI.StationaryNS.homogeneousDatum_measurable line 230
theorem OAI.StationaryNS.homogeneousDatum_sq_locallyIntegrable line 243
Source documentation
Local square integrability, including the singular point.
```
theorem homogeneousDatum_sq_locallyIntegrable :
    LocallyIntegrable (fun x : Space => ‖homogeneousDatum x‖ ^ 2) := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum
theorem OAI.StationaryNS.homogeneousDatum_memLp_two_on_compact line 262
Source documentation
The datum belongs to L² on every compact subset of three-dimensional space.
```
theorem homogeneousDatum_memLp_two_on_compact {K : Set Space} (hK : IsCompact K) :
    MemLp homogeneousDatum 2 (volume.restrict K) := by
…
```
Mentions: OAI.StationaryNS.Space, OAI.StationaryNS.homogeneousDatum