The -part of vanishes exactly where the -density vanishes
ProvedFiniteEnergyPlane.piDs_ne_zero_iff_dlambdaDensity_posLet be a strictly star-shaped level with Liouville form , Reeb field and contact structure , let be a -compatible complex structure on , and the induced almost complex structure on . Let be open and be -holomorphic, with . Then for every ,
where is the projection along , and is read in Hryniewicz's global frame of .
So the zeros of are exactly the points where the integrand vanishes, and elsewhere this integrand is positive. This lets statements about the -density be transferred to the section and back.
Formalization Note is V 1, is Jtilde H J, proj H ∘ u; in the global frame is piDs H u z (a complex number, xiCoordC), and is dlambdaDensity H u z. The hypotheses only ask that avoid and be -holomorphic on the open set (no energy bound).
import Definitions.Def_FiniteEnergyPlane_Winding
namespace FiniteEnergyPlane
open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real
/-- At a point `z` of an open set `U` on which `u` avoids `0` and is `J̃`-holomorphic, the
`ξ`-component `π ∂ₛu(z)` is nonzero exactly when the `dλ`-density of `u` at `z` is positive. -/
theorem piDs_ne_zero_iff_dlambdaDensity_pos (H : V 1 → ℝ) (hH : IsStrictlyStarShapedLevel H)
(J : V 1 → V 1 →L[ℝ] V 1) (hJ : IsCompatibleXiStructure H J) (U : Set ℂ) (hU : IsOpen U)
(u : ℂ → V 1) (hu0 : ∀ z ∈ U, u z ≠ 0)
(hhol : JHolomorphic.IsJHolomorphicOn (Jtilde H J) U u) {z : ℂ} (hz : z ∈ U) :
piDs H u z ≠ 0 ↔ 0 < dlambdaDensity H u z := by
sorry
end FiniteEnergyPlane