OAI/Analysis/Mahler/SphereDensityRestriction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.exists_outward_tangent_frame line 10

   Source documentation

   Pointwise adapted tangent frames suffice; no global tangent frame is chosen or assumed continuous.

   theorem exists_outward_tangent_frame {k : ℕ} {x : ComplexEuclidean (k+1)} (hx : ‖x‖ = 1) :
       ∃ v : Fin (2*k+1) → ComplexEuclidean (k+1),
         (∀ i, inner ℝ x (v i) = 0) ∧ sphereVolume k (Matrix.vecCons x v) = 1 := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereVolume

2. theorem OAI.Mahler.orientedDensity_congr_on_tangent line 28

   Source documentation

   The ambient cofactor formula depends only on the actual tangent restriction of the boundary form.

   theorem orientedDensity_congr_on_tangent {k : ℕ} {x : ComplexEuclidean (k+1)}
       (hx : ‖x‖ = 1)
       {B C : ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ}
       (h : ∀ v : Fin (2*k+1) → ComplexEuclidean (k+1),
         (∀ i, inner ℝ x (v i) = 0) → B v = C v) :
       orientedDensity (sphereFrame k) (sphereVolume k) B x =
         orientedDensity (sphereFrame k) (sphereVolume k) C x := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.orientedDensity, OAI.Mahler.sphereFrame, OAI.Mahler.sphereVolume

3. lemma OAI.Mahler.orientedDensity_zero line 43