FlatTubeArea.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.flatTubeFrame line 19
Source comment
In a flat normal chart the final normal coordinate is one, and the transverse column is the fixed negative final basis vector.
```
def flatTubeFrame (Y : S × E → E) (x : S × E) (bS : Module.Basis ι ℝ S)
    (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E) : ι ⊕ (κ ⊕ Unit) → S × E :=
…
```
lemma OAI.AffineBernstein.flatTubeFrame_matrix line 26
lemma OAI.AffineBernstein.flatTubeFrame_det line 55
lemma OAI.AffineBernstein.flat_supportConormal_transverse line 65
def OAI.AffineBernstein.flatTubeAffineAreaJet line 70

lemma OAI.AffineBernstein.flatTubeAffineAreaJet_eq line 80

Source comment

Literal flat-normal-chart area density. No sphere measure change is required to obtain the local variational equation in these coordinates.

lemma flatTubeAffineAreaJet_eq {H : S × E → ℝ} {Y : S × E → E} {x : S × E}
    (hH : ContDiffAt ℝ ∞ H x) (hY : ContDiffAt ℝ ∞ Y x)
    (heul : H =ᶠ[nhds x] (fun q => inner ℝ q.2 (Y q)))
    (hgrad : ∀ᶠ q in nhds x, ∀ z : E, fderiv ℝ H q (0,z) = inner ℝ (Y q) z)
    (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    (hB : 0 < (tubeBaseMatrix H x bS).det) (hR : 0 < (tubeRadiusMatrix H x bE).det) :
    flatTubeAffineAreaJet H Y x bS bE = tubeAreaDensity (tubeBaseMatrix H x bS)
      (tubeRadiusMatrix H x bE) (1/((Fintype.card ι : ℝ)+Fintype.card κ+2)) := by
…

Mentions: OAI.AffineBernstein.tubeBaseMatrix, OAI.AffineBernstein.tubeRadiusMatrix, OAI.AffineBernstein.flatTubeAffineAreaJet, OAI.AffineBernstein.tubeAreaDensity