SphereOrientation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.interleavedBasis_orthonormal line 12
Source documentation
The coordinate frame used in the flux density is Euclidean orthonormal.
```
lemma interleavedBasis_orthonormal (n : ℕ) : Orthonormal ℝ (interleavedBasis (n := n)) := by
…
```
Mentions: OAI.Mahler.interleavedBasis
lemma OAI.Mahler.sphereFluxFrame_orthonormal line 24
lemma OAI.Mahler.sphereNormal_outward line 32
lemma OAI.Mahler.sphereNormal_tangent line 39
lemma OAI.Mahler.sphereDilation_surjective line 45
lemma OAI.Mahler.continuous_radiusFluxDensity line 56
def OAI.Mahler.radiusSphereFlux line 77
Source documentation
Flux on the radius-r sphere itself. For nonpositive radii we use zero; this branch is irrelevant to the right-sided small-sphere limit.
```
noncomputable def radiusSphereFlux (k : ℕ) (u : ComplexEuclidean (k+1) → ℂ) (r : ℝ) : ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean

theorem OAI.Mahler.radiusSphereFlux_eq_small line 85

Source documentation

No measurability premise is needed: C2 regularity supplies it.

theorem radiusSphereFlux_eq_small {k : ℕ} {u : ComplexEuclidean (k+1) → ℂ}
    (r : ℝ) (hr : 0 < r)
    (hu : ∀ z : sphere (0 : ComplexEuclidean (k+1)) r,
      ContDiffAt ℝ 2 u (z : ComplexEuclidean (k+1))) :
    radiusSphereFlux k u r = smallSphereFlux k u r := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.radiusSphereFlux, OAI.Mahler.smallSphereFlux