OrientedSphereDensity.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.orientedDensity line 19
Source documentation
Outward surface coefficient in an ambient orthonormal frame. Division by Ω b fixes the orientation to the specified ambient volume form. At a unit normal x this is the cofactor formula for the restriction of B to x-perp.
```
noncomputable def orientedDensity (b : OrthonormalBasis (Fin (d+1)) ℝ E)
    (Ω : E [⋀^Fin (d+1)]→ₗ[ℝ] ℂ) (B : E [⋀^Fin d]→ₗ[ℝ] ℂ) (x : E) : ℂ :=
…
```
lemma OAI.Mahler.volume_update_basis line 23
lemma OAI.Mahler.volume_cons_remove line 35
theorem OAI.Mahler.orientedDensity_contraction line 47
Source documentation
The cofactor density of contraction of ambient volume by the outward radial vector is exactly norm squared, with positive sign.
```
theorem orientedDensity_contraction (b : OrthonormalBasis (Fin (d+1)) ℝ E)
    (Ω : E [⋀^Fin (d+1)]→ₗ[ℝ] ℂ) (hΩ : Ω b ≠ 0) (x : E) :
    orientedDensity b Ω (Ω.curryLeft x) x = (‖x‖^2 : ℝ) := by
…
```
Mentions: OAI.Mahler.orientedDensity
lemma OAI.Mahler.orientedDensity_smul line 67
def OAI.Mahler.normalWedge line 80
Source documentation
Exterior multiplication by the normal covector, expressed by the standard alternating sum. It is used only to verify the surface density.
```
noncomputable def normalWedge (x : E) (B : E [⋀^Fin d]→ₗ[ℝ] ℂ) :
    E [⋀^Fin (d+1)]→ₗ[ℝ] ℂ :=
…
```
lemma OAI.Mahler.normalWedge_basis line 84
lemma OAI.Mahler.orientedDensity_eq_normalWedge line 97
theorem OAI.Mahler.normalWedge_outward_tangent line 105
Source documentation
On a unit sphere, the normal wedge evaluates on outward normal followed by tangent vectors as exactly the boundary form. This checks the sign and shows which surface restriction the cofactor formula represents.
```
theorem normalWedge_outward_tangent (B : E [⋀^Fin d]→ₗ[ℝ] ℂ) {x : E}
    (hx : ‖x‖ = 1) (v : Fin d → E) (hv : ∀ i, inner ℝ x (v i) = 0) :
    normalWedge x B (Matrix.vecCons x v) = B v := by
…
```
Mentions: OAI.Mahler.normalWedge
lemma OAI.Mahler.topForm_ext_on_basis line 118
lemma OAI.Mahler.normalWedge_eq_density_smul line 127

theorem OAI.Mahler.orientedDensity_spec line 137

Source documentation

The density multiplies the outward area form to give the actual restriction of B to every tuple of tangent vectors.

theorem orientedDensity_spec (b : OrthonormalBasis (Fin (d+1)) ℝ E)
    (Ω : E [⋀^Fin (d+1)]→ₗ[ℝ] ℂ) (hΩ : Ω b ≠ 0)
    (B : E [⋀^Fin d]→ₗ[ℝ] ℂ) {x : E} (hx : ‖x‖ = 1)
    (v : Fin d → E) (hv : ∀ i, inner ℝ x (v i) = 0) :
    B v = orientedDensity b Ω B x * Ω (Matrix.vecCons x v) := by
…

Mentions: OAI.Mahler.orientedDensity

theorem OAI.Mahler.orientedDensity_frame_independent line 147

Source documentation

Cofactor density is independent of the ambient orthonormal frame. Both frames use the same specified source orientation Ω.

theorem orientedDensity_frame_independent
    (b c : OrthonormalBasis (Fin (d+1)) ℝ E)
    (Ω : E [⋀^Fin (d+1)]→ₗ[ℝ] ℂ) (hb : Ω b ≠ 0) (hc : Ω c ≠ 0)
    (B : E [⋀^Fin d]→ₗ[ℝ] ℂ) (x : E) :
    orientedDensity b Ω B x = orientedDensity c Ω B x := by
…

Mentions: OAI.Mahler.orientedDensity