Bochner-valued selected-block Fubini for R-322/R-324

The first selected-coordinate theorem was stated for real-valued kernels. R-324 carries a signed complex Fourier factor outside the real primitive kernel, so this file records the same exact product-measure reindex for an arbitrary complete real normed target. It also gives the concrete Finset (Fin m) adapter used by the block selectors.

Complete normed target

theorem Anderson4D.integral_pi_eq_integral_complement_integral_selected_bochner {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Fintype ι] [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ] (selected : ι → Prop) [DecidablePred selected] (f : (ι → X) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : ι) => μ)) : (∫ (x : ι → X), f x ∂MeasureTheory.Measure.pi fun (x : ι) => μ) = ∫ (xC : { i : ι // ¬selected i } → X), ∫ (xB : { i : ι // selected i } → X), f ((MeasurableEquiv.piEquivPiSubtypeProd (fun (x : ι) => X) selected).symm (xB, xC)) ∂MeasureTheory.Measure.pi fun (x : { i : ι // selected i }) => μ ∂MeasureTheory.Measure.pi fun (x : { i : ι // ¬selected i }) => μ

Exact selected/complement Fubini reindex for a complete Bochner-valued integrand. In particular, this applies with E = ℂ.

Concrete finite-index block adapter

def Anderson4D.r322SelectedFinPredicate {m : ℕ} (B : Finset (Fin m)) (i : Fin m) : Prop

Predicate form of membership in a selected Fin block. Keeping this as a named predicate gives the selected and complementary subtype products the same canonical Subtype.fintype instances as the generic theorem.

Equations

• Anderson4D.r322SelectedFinPredicate B i = (i ∈ B)

@[implicit_reducible]

instance Anderson4D.r322SelectedFinPredicate_decidable {m : ℕ} (B : Finset (Fin m)) : DecidablePred (r322SelectedFinPredicate B)

Equations

• Anderson4D.r322SelectedFinPredicate_decidable B i = Anderson4D.r322SelectedFinPredicate_decidable._aux_1 B i

@[simp]

theorem Anderson4D.r322SelectedFinPredicate_iff {m : ℕ} (B : Finset (Fin m)) (i : Fin m) : r322SelectedFinPredicate B i ↔ i ∈ B

def Anderson4D.r322MergeSelectedFinCoordinates {m : ℕ} {X : Type u_1} (B : Finset (Fin m)) (xB : { i : Fin m // r322SelectedFinPredicate B i } → X) (xC : { i : Fin m // ¬r322SelectedFinPredicate B i } → X) : Fin m → X

Reassemble a Fin m tuple from its selected block coordinates and its complementary coordinates.

Equations

• Anderson4D.r322MergeSelectedFinCoordinates B xB xC = (Equiv.piEquivPiSubtypeProd (Anderson4D.r322SelectedFinPredicate B) fun (x : Fin m) => X).symm (xB, xC)

@[simp]

theorem Anderson4D.r322MergeSelectedFinCoordinates_apply_mem {m : ℕ} {X : Type u_1} (B : Finset (Fin m)) (xB : { i : Fin m // r322SelectedFinPredicate B i } → X) (xC : { i : Fin m // ¬r322SelectedFinPredicate B i } → X) (i : Fin m) (hi : i ∈ B) : r322MergeSelectedFinCoordinates B xB xC i = xB ⟨i, hi⟩

@[simp]

theorem Anderson4D.r322MergeSelectedFinCoordinates_apply_not_mem {m : ℕ} {X : Type u_1} (B : Finset (Fin m)) (xB : { i : Fin m // r322SelectedFinPredicate B i } → X) (xC : { i : Fin m // ¬r322SelectedFinPredicate B i } → X) (i : Fin m) (hi : i ∉ B) : r322MergeSelectedFinCoordinates B xB xC i = xC ⟨i, hi⟩

theorem Anderson4D.integral_fin_pi_eq_integral_complement_integral_block_bochner {m : ℕ} {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ] (B : Finset (Fin m)) (f : (Fin m → X) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin m) => μ)) : (∫ (x : Fin m → X), f x ∂MeasureTheory.Measure.pi fun (x : Fin m) => μ) = ∫ (xC : { i : Fin m // ¬r322SelectedFinPredicate B i } → X), ∫ (xB : { i : Fin m // r322SelectedFinPredicate B i } → X), f (r322MergeSelectedFinCoordinates B xB xC) ∂MeasureTheory.Measure.pi fun (x : { i : Fin m // r322SelectedFinPredicate B i }) => μ ∂MeasureTheory.Measure.pi fun (x : { i : Fin m // ¬r322SelectedFinPredicate B i }) => μ

Finset (Fin m) specialization of the exact Bochner Fubini split. The selected block is the inner integral and the complement remains the outer parameter tuple.