noncomputable def continuousLocationDualTupleScale {ι : Type v} (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] (weights : ContinuousLocationWeights ι) : (PiLp 2 fun (x : ι) => E) →L[ℝ] PiLp 2 fun (x : ι) => E

The componentwise scaling u_j ↦ √m_j • u_j on the Hilbert product PiLp 2 (fun _ : ι ↦ E) behind the weighted tuple geometry.

theorem continuousLocationDualTupleScale_apply {ι : Type v} {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (weights : ContinuousLocationWeights ι) (u : PiLp 2 fun (x : ι) => E) (j : ι) : ((continuousLocationDualTupleScale E weights) u).ofLp j = √↑(weights j) • u.ofLp j

The j-th coordinate of continuousLocationDualTupleScale E weights u is √m_j • u_j.

noncomputable def continuousLocationDualTupleSeminorm {ι : Type v} [Fintype ι] (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (weights : ContinuousLocationWeights ι) : Seminorm ℝ (PiLp 2 fun (x : ι) => E)

The weighted tuple geometry of Proposition 6.17, owned canonically as the pullback of the ambient Hilbert norm on PiLp 2 (fun _ : ι ↦ E) along continuousLocationDualTupleScale E weights.

theorem continuousLocationDualTupleSeminorm_eq_norm_scale {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) (u : PiLp 2 fun (x : ι) => E) : (continuousLocationDualTupleSeminorm E weights) u = ‖(continuousLocationDualTupleScale E weights) u‖

Evaluating continuousLocationDualTupleSeminorm E weights gives the ambient norm of the weighted scaling of the tuple.

theorem continuousLocationDualTupleSeminorm_apply {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) (u : ι → E) : (continuousLocationDualTupleSeminorm E weights) (WithLp.toLp 2 u) = continuousLocationDualTupleNorm E weights u

The seminorm owner continuousLocationDualTupleSeminorm E weights recovers the textbook weighted tuple norm continuousLocationDualTupleNorm E weights after identifying coordinate tuples with the Hilbert product PiLp 2 (fun _ : ι ↦ E).

instance continuousLocationDualTupleSeminorm.isNorm {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) : (continuousLocationDualTupleSeminorm E weights).IsNorm

Positive weights make the pullback seminorm continuousLocationDualTupleSeminorm E weights nondegenerate, so the weighted tuple geometry is a genuine norm.

@[reducible, inline]

noncomputable abbrev continuousLocationSmoothingMapPiLp {ι : Type v} [Fintype ι] (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (weights : ContinuousLocationWeights ι) : E →L[ℝ] (PiLp 2 fun (x : ι) => E) →L[ℝ] ℝ

The canonical PiLp transport of continuousLocationSmoothingMap E weights, viewed in the weighted tuple geometry on PiLp 2 (fun _ : ι ↦ E). This is a thin bridge from the source-facing coordinate-tuple owner to the Hilbert-product realization used by continuousLocationDualTupleSeminorm E weights.

theorem continuousLocationSmoothingMapPiLp_apply {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) (x : E) (u : PiLp 2 fun (x : ι) => E) : ((continuousLocationSmoothingMapPiLp E weights) x) u = ∑ j : ι, ↑(weights j) * inner ℝ (u.ofLp j) x

Evaluating the transported smoothing operator on a PiLp tuple recovers the same weighted pairing formula as continuousLocationSmoothingMap_apply.

theorem continuousLocation_totalPopulation_pos {ι : Type v} [Fintype ι] (weights : ContinuousLocationWeights ι) [Nonempty ι] : 0 < continuousLocationTotalPopulation weights

Helper for Proposition 6.17: if the index type is nonempty, then the total population weight is strictly positive.

theorem continuousLocation_weighted_constant_tuple_norm {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) (x : E) : ‖WithLp.toLp 2 fun (j : ι) => √↑(weights j) • x‖ = √(continuousLocationTotalPopulation weights) * ‖x‖

Helper for Proposition 6.17: the weighted constant tuple has ambient PiLp norm √P * ‖x‖.

theorem continuousLocation_pairing_le_sqrt_total_mul_norm_mul_seminorm {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) (x : E) (u : PiLp 2 fun (x : ι) => E) : ∑ j : ι, ↑(weights j) * inner ℝ (u.ofLp j) x ≤ √(continuousLocationTotalPopulation weights) * ‖x‖ * (continuousLocationDualTupleSeminorm E weights) u

Helper for Proposition 6.17: the weighted pairing is controlled by the product of the source norm and the weighted tuple seminorm.

theorem continuousLocation_constant_unit_witness {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (weights : ContinuousLocationWeights ι) [Nonempty ι] {e : E} (he : ‖e‖ = 1) : (continuousLocationDualTupleNorm E weights fun (x : ι) => (√(continuousLocationTotalPopulation weights))⁻¹ • e) = 1 ∧ ∑ j : ι, ↑(weights j) * inner ℝ ((√(continuousLocationTotalPopulation weights))⁻¹ • e) e = √(continuousLocationTotalPopulation weights)

Helper for Proposition 6.17: the normalized constant tuple has weighted norm 1 and attains the pairing value √P against the same unit vector.

theorem continuousLocationSmoothingMap_primalDualOperatorNorm_eq_sqrt_totalPopulation {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] [FiniteDimensional ℝ E] [Nontrivial E] (weights : ContinuousLocationWeights ι) : (normSeminorm ℝ E).primalDualOperatorNorm (continuousLocationDualTupleSeminorm E weights) ↑(continuousLocationSmoothingMapPiLp E weights) = √(continuousLocationTotalPopulation weights)

Canonical owner form of Proposition 6.17: the induced norm of the continuous-location smoothing map from the ambient norm on E to the weighted dual-tuple geometry is √P, where P = \sum_j m_j is the total population weight. The PiLp realization is exposed through the thin bridge continuousLocationSmoothingMapPiLp E weights, so the public theorem stays on Seminorm.primalDualOperatorNorm without leaking the transport term.

theorem continuousLocation_sSup_pairing_unitSpheres_eq_sqrt_totalPopulation {ι : Type v} {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] [FiniteDimensional ℝ E] [Nontrivial E] (weights : ContinuousLocationWeights ι) : sSup ((fun (xu : E × (ι → E)) => ∑ j : ι, ↑(weights j) * inner ℝ (xu.2 j) xu.1) '' (Metric.sphere 0 1).prod {u : ι → E | continuousLocationDualTupleNorm E weights u = 1}) = √(continuousLocationTotalPopulation weights)

Proposition 6.17: rewriting the canonical induced-norm statement through continuousLocationSmoothingMap_primalDualOperatorNorm_eq_sqrt_totalPopulation, Seminorm.primalDualOperatorNorm_eq_sSup_dualPairing, continuousLocationSmoothingMap_apply, and continuousLocationDualTupleSeminorm_apply, and then transporting back along PiLp.continuousLinearEquiv, gives the source-facing unit-sphere formula for the weighted pairing.