Documentation

TauCeti.MeasureTheory.Function.AreaFormula.Multiplicity

The area formula with multiplicity #

The weighted area formula integrates the geometric Jacobian on the parameter space and sums the weights over each fiber in the target. Fiber sums take values in ℝ≥0∞: in particular an infinite fiber has infinite multiplicity, not multiplicity zero. The target measure is normalized Euclidean Hausdorff measure.

We sum the injective area formula over measurable bi-Lipschitz pieces of the regular locus. The remaining points have null image, by Rademacher's theorem and the null-image result for zero Jacobians.

For a self-map f : E → E of a finite-dimensional inner product space, the area formula on a measurable set s of points with invertible derivative says that f pushes |det Df(x)| dx on s forward to the fibre-counting density y ↦ #(s ∩ f⁻¹(y)) (TauCeti.map_withDensity_abs_det_fderiv_eq_withDensity_encard), giving a Bochner area formula and an integrability transfer when almost every fibre meets s in a finite set. Splitting the measurable sets where the Jacobian is positive and negative gives the signed area formula (TauCeti.integral_det_fderiv_smul_comp_eq_integral_ncard_sub_ncard_smul): for a differentiable map with almost every fibre finite, a strongly measurable g, and det Df • g ∘ f integrable,

∫ det Df(x) • g (f x) dx = ∫ (N⁺(y) - N⁻(y)) • g(y) dy,

where N^±(y) is the number of preimages of y at which det Df is positive, respectively negative.

Main results #

References #

source
theorem TauCeti.measurable_tsum_fiber_of_injective_fderiv {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] [SecondCountableTopology V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {g : U → ENNReal} (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hg : Measurable g) :
Measurable fun (y : V) => ∑' (x : ↑(s ∩ f ⁻¹' {y})), g ↑x

Weighted fiber sums for a map with injective derivative are measurable. Such a map need not itself be injective or globally Lipschitz.

source
theorem TauCeti.lintegral_normDet_fderiv_mul_eq_lintegral_tsum_of_injective_fderiv {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {g : U → ENNReal} (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hinj : ∀ x ∈ s, Function.Injective ⇑(fderiv ℝ f x)) (hg : Measurable g) :
∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet * g x = ∫⁻ (y : V), ∑' (x : ↑(s ∩ f ⁻¹' {y})), g ↑x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)

The weighted area formula on a measurable set of points with injective derivative, without any injectivity assumption on the parametrization itself.

source
theorem TauCeti.tsum_fiber_inter_setOf_regular_ae_eq {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : U → V} (s : Set U) (g : U → ENNReal) {K : NNReal} (hf : LipschitzWith K f) :
(fun (y : V) => ∑' (x : ↑(s ∩ {x : U | DifferentiableAt ℝ f x ∧ (↑(fderiv ℝ f x)).normDet ≠ 0} ∩ f ⁻¹' {y})), g ↑x) =ᵐ[MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)] fun (y : V) => ∑' (x : ↑(s ∩ f ⁻¹' {y})), g ↑x

Restricting the parameters of a Lipschitz map to its differentiability points with nonzero Jacobian preserves weighted fiber sums almost everywhere for normalized Hausdorff measure. Neither the parameter set nor the weight needs to be measurable.

source
theorem LipschitzWith.tsum_fiber_congr_ae {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [MeasurableSpace U] [BorelSpace U] [EMetricSpace V] [MeasurableSpace V] [BorelSpace V] {f : U → V} {K : NNReal} (hf : LipschitzWith K f) {s t : Set U} (hst : s =ᵐ[MeasureTheory.volume] t) (g : U → ENNReal) :
(fun (y : V) => ∑' (x : ↑(s ∩ f ⁻¹' {y})), g ↑x) =ᵐ[MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)] fun (y : V) => ∑' (x : ↑(t ∩ f ⁻¹' {y})), g ↑x

Changing the parameter set on a Lebesgue-null set changes its weighted fiber sums only on a Hausdorff-null set. No measurability of the weight or the sets is needed.

source
theorem LipschitzWith.aemeasurable_tsum_fiber {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {g : U → ENNReal} {K : NNReal} (hf : LipschitzWith K f) (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hg : Measurable g) :
AEMeasurable (fun (y : V) => ∑' (x : ↑(s ∩ f ⁻¹' {y})), g ↑x) (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U))

Weighted fiber sums of a Lipschitz map on a Lebesgue-measurable set are almost everywhere measurable for normalized Hausdorff measure, including infinite fibers.

source
theorem LipschitzWith.lintegral_normDet_fderiv_mul_eq_lintegral_tsum {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {g : U → ENNReal} {K : NNReal} (hf : LipschitzWith K f) (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hg : Measurable g) :
∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet * g x = ∫⁻ (y : V), ∑' (x : ↑(s ∩ f ⁻¹' {y})), g ↑x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)

The weighted area formula with multiplicity. Integrating the geometric Jacobian of a Lipschitz map against a nonnegative measurable weight equals the normalized Hausdorff integral of the sum of the weights over each fiber. The parameter set may be Lebesgue measurable rather than Borel, and infinite fibers use extended sums.

source
theorem LipschitzWith.lintegral_normDet_fderiv_eq_lintegral_encard {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U] [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {K : NNReal} (hf : LipschitzWith K f) (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) :
∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet = ∫⁻ (y : V), ↑(s ∩ f ⁻¹' {y}).encard ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)

The unweighted area formula: multiplicity is the extended cardinality of the fiber, so infinite fibers are counted as infinity.

source
theorem TauCeti.measurable_encard_inter_preimage_singleton {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → E} {s : Set E} (hs : MeasurableSet s) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hdet : ∀ x ∈ s, (fderiv ℝ f x).det ≠ 0) :
Measurable fun (y : E) => ↑(s ∩ f ⁻¹' {y}).encard

The number of points of a fibre of f lying in a measurable set s of points where f is differentiable with invertible derivative is a measurable function of the base point, with values in ℕ∞.

source
theorem TauCeti.map_withDensity_abs_det_fderiv_eq_withDensity_encard {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → E} {s : Set E} (hs : MeasurableSet s) (hf : Measurable f) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hdet : ∀ x ∈ s, (fderiv ℝ f x).det ≠ 0) :
MeasureTheory.Measure.map f ((MeasureTheory.volume.restrict s).withDensity fun (x : E) => ENNReal.ofReal |(fderiv ℝ f x).det|) = MeasureTheory.volume.withDensity fun (y : E) => ↑(s ∩ f ⁻¹' {y}).encard

The pushforward of the Jacobian measure counts preimages. On a measurable set s of points where f is differentiable with invertible derivative, f pushes the measure |det Df(x)| dx on s forward to the measure with density y ↦ #(s ∩ f⁻¹(y)), an extended natural number. This is the non-injective form of MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar.

source
theorem TauCeti.setIntegral_abs_det_fderiv_smul_comp_eq_integral_ncard_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → E} {s : Set E} (hs : MeasurableSet s) (hf : Measurable f) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hdet : ∀ x ∈ s, (fderiv ℝ f x).det ≠ 0) (hfin : ∀ᵐ (y : E), (s ∩ f ⁻¹' {y}).Finite) {g : E → F} (hg : MeasureTheory.StronglyMeasurable g) :
∫ (x : E) in s, |(fderiv ℝ f x).det| • g (f x) = ∫ (y : E), ↑(s ∩ f ⁻¹' {y}).ncard • g y

The area formula with multiplicity on a set of regular points. If f is differentiable with invertible derivative on a measurable set s, and almost every fibre of f meets s in a finite set, then ∫_s |det Df(x)| • g (f x) dx = ∫ #(s ∩ f⁻¹(y)) • g(y) dy.

source
theorem TauCeti.integrable_ncard_smul_of_integrableOn_abs_det_fderiv_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → E} {s : Set E} (hs : MeasurableSet s) (hf : Measurable f) (hd : ∀ x ∈ s, DifferentiableAt ℝ f x) (hdet : ∀ x ∈ s, (fderiv ℝ f x).det ≠ 0) (hfin : ∀ᵐ (y : E), (s ∩ f ⁻¹' {y}).Finite) {g : E → F} (hg : MeasureTheory.StronglyMeasurable g) (hint : MeasureTheory.IntegrableOn (fun (x : E) => |(fderiv ℝ f x).det| • g (f x)) s MeasureTheory.volume) :
MeasureTheory.Integrable (fun (y : E) => ↑(s ∩ f ⁻¹' {y}).ncard • g y) MeasureTheory.volume

Under the hypotheses of TauCeti.setIntegral_abs_det_fderiv_smul_comp_eq_integral_ncard_smul, if |det Df(x)| • g (f x) is integrable on s, then y ↦ #(s ∩ f⁻¹(y)) • g(y) is integrable.

source
theorem TauCeti.integral_det_fderiv_smul_comp_eq_integral_ncard_sub_ncard_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → E} (hf : Differentiable ℝ f) (hfin : ∀ᵐ (y : E), (f ⁻¹' {y}).Finite) {g : E → F} (hg : MeasureTheory.StronglyMeasurable g) (hint : MeasureTheory.Integrable (fun (x : E) => (fderiv ℝ f x).det • g (f x)) MeasureTheory.volume) :
∫ (x : E), (fderiv ℝ f x).det • g (f x) = ∫ (y : E), (↑({x : E | 0 < (fderiv ℝ f x).det} ∩ f ⁻¹' {y}).ncard - ↑({x : E | (fderiv ℝ f x).det < 0} ∩ f ⁻¹' {y}).ncard) • g y

The signed area formula. Let f : E → E be differentiable with almost every fibre finite, and let det Df(x) • g (f x) be integrable. Then its integral is the integral of g weighted by the number of preimages at which det Df is positive minus the number at which it is negative. Points with det Df(x) = 0 contribute to neither side.