SourcePrimitiveStokes.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.MassHypotheses.sourceHomogeneousPrimitive_flux_zero line 13

Source documentation

C2 on the punctured space follows from the mass hypotheses. The exact-form flux vanishes in every complex dimension at least two.

theorem MassHypotheses.sourceHomogeneousPrimitive_flux_zero {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
    (t : ℝ) :
    sphereFlux (k+1) (fun x =>
      (extDeriv (sourceHomogeneousPrimitive (m := m) G t) x).toAlternatingMap) = 0 := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.sphereFlux, OAI.Mahler.sourceHomogeneousPrimitive

theorem OAI.Mahler.sphereFlux_eq_zero_of_tangent_exact_C2 line 28

Source documentation

A form agreeing pointwise on sphere tangent tuples with a fixed real scalar multiple of an exact form has zero sphere flux.

theorem sphereFlux_eq_zero_of_tangent_exact_C2 {k : ℕ}
    (B : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ)
    (eta : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k)]→L[ℝ] ℂ)
    (c : ℝ) (hreg : ContDiffOn ℝ 2 eta ({0}ᶜ))
    (he : ∀ x, ‖x‖ = 1 → ∀ v : Fin (2*k+1) → ComplexEuclidean (k+1),
      (∀ i, inner ℝ x (v i) = 0) → B x v = (c : ℂ) * extDeriv eta x v) :
    sphereFlux k B = 0 := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereFlux

theorem OAI.Mahler.MassHypotheses.sourcePrimitive_representation_C2 line 54