Null affine hyperplanes in finite real products

This file proves that the solution set of a nontrivial weighted affine equation in a finite product of real lines is a null set for the product measure. Coordinate and coordinate-sum hyperplanes are recorded as volume corollaries.

This is the finite-product companion of Measure.pi_hyperplane. The corresponding statement for a proper affine subspace of a finite-dimensional real space is addHaar_affineSubspace; the lemmas here avoid that Haar/affine-subspace API.

This is a temporary project home. Intended Mathlib placement:

• pi_weighted_hyperplane, ae_weighted_hyperplane → Mathlib.MeasureTheory.Constructions.Pi, after pi_hyperplane / ae_eval_ne

The volume wrappers volume_setOf_eval_eq and volume_setOf_fin_sum_eq are local conveniences for the present project.

TODO: if those lemmas land in Mathlib, delete this file and switch uses to the upstream names.

theorem MeasureTheory.Measure.pi_weighted_hyperplane {ι : Type u_1} [Fintype ι] (μ : ι → Measure ℝ) [∀ (j : ι), SigmaFinite (μ j)] (a : ι → ℝ) (i : ι) [NullSingletonClass (μ i)] (hi : a i ≠ 0) (c : ℝ) : (Measure.pi μ) {x : ι → ℝ | ∑ j : ι, a j * x j = c} = 0

A level set of a weighted coordinate sum has product measure zero if one of its coefficients is nonzero. This is the finite-product form of the fact that a proper affine hyperplane is Lebesgue-null; compare pi_hyperplane and addHaar_affineSubspace.

theorem MeasureTheory.Measure.ae_weighted_hyperplane {ι : Type u_1} [Fintype ι] (μ : ι → Measure ℝ) [∀ (j : ι), SigmaFinite (μ j)] (a : ι → ℝ) (i : ι) [NullSingletonClass (μ i)] (hi : a i ≠ 0) (c : ℝ) : ∀ᵐ (x : ι → ℝ) ∂Measure.pi μ, ∑ j : ι, a j * x j ≠ c

Almost every point of a finite real product lies off a nontrivial weighted hyperplane.

theorem MeasureTheory.Measure.volume_setOf_fintype_weighted_sum_eq {ι : Type u_1} [Fintype ι] (a : ι → ℝ) (i : ι) (hi : a i ≠ 0) (c : ℝ) : volume {x : ι → ℝ | ∑ j : ι, a j * x j = c} = 0

A level set of a weighted coordinate sum in a finite real product has volume zero if one of its coefficients is nonzero.

theorem MeasureTheory.Measure.volume_setOf_eval_eq {ι : Type u_1} [Fintype ι] (i : ι) (c : ℝ) : volume {x : ι → ℝ | x i = c} = 0

A level set of a coordinate projection in a finite real product has volume zero.

theorem MeasureTheory.Measure.volume_setOf_fintype_sum_eq {ι : Type u_1} [Fintype ι] [Nonempty ι] (c : ℝ) : volume {x : ι → ℝ | ∑ i : ι, x i = c} = 0

A level set of the coordinate sum in a nonempty finite real product has volume zero. The nonempty hypothesis is necessary: in dimension zero the level set at zero is the whole space.

theorem MeasureTheory.Measure.volume_setOf_fin_sum_eq {n : ℕ} (hn : 0 < n) (c : ℝ) : volume {x : Fin n → ℝ | ∑ i : Fin n, x i = c} = 0

A level set of the coordinate sum in a nonempty finite real product has volume zero.