chore: privatize 4 same-file helpers + drop 7 dead @[simp] lemmas in InfraCore (#111)

* chore: privatize 4 same-file-only helper lemmas

Privatize lemmas with zero references anywhere in the repository (including
blueprint, docs, and the wider `Exchangeability/` tree) whose only callers
live in the same file:

* `ViaKoopman/CesaroL2ToL1.lean`: `iterate_shift_eval'`, `iterate_shift_eval0'`
  — proof-step helpers; only in-file caller of each.
* `Ergodic/ShiftInvariantRepresentatives.lean`: `ae_shift_invariance_on_rep`
  — proof helper; only caller at L338 in the same file.
* `Util/ProductBounds.lean`: `abs_prod_le_one` — only caller is its sibling
  `abs_prod_sub_prod_le` directly below. Updated the file's docstring to
  drop the now-private name from "Main results".

Candidate set produced by an audit script that enumerates non-private
`lemma`/`theorem` declarations, excludes anything with a tactic-database
attribute (`@[simp]`, `@[measurability]`, `@[fun_prop]`, etc.) where
grep can't see implicit use, and reports those with zero `git grep -lw`
hits outside their owner file. The audit found 25 candidates; the other
21 were judged to be real public API on public namespaces
(`Contractable.*`, `Exchangeable.*`, `Integrable.of_abs_bounded`,
`fixedSubspace_closed`, etc.) and left as-is even though no internal
caller currently uses them.

* chore(InfraCore): drop 7 dead @[simp] lemmas (probe verified, all unused)

Following the standard "delete + build" probe pattern (since `@[simp]`
lemmas can be used implicitly and grep can't see those uses), I removed
seven `@[simp]` lemmas in `ViaKoopman/InfraCore.lean` and confirmed via
`lake build` that none was load-bearing in any simp call across the
3527-job build:

* `shiftℤ_apply`, `shiftℤInv_apply`, `restrictNonneg_apply` — `rfl`
  unfolding lemmas for `shiftℤ`/`shiftℤInv`/`restrictNonneg`.
* `shiftℤ_comp_shiftℤInv`, `shiftℤInv_comp_shiftℤ` — round-trip identities
  for the two-sided shift and its inverse.
* `restrictNonneg_extendByZero`, `extendByZero_apply_nat` — interaction
  lemmas for the nonneg-restrict / extend-by-zero pair.

All seven had zero named references outside their owning file; the probe
confirms that holds at the simp level too. If a future caller needs any
of them, re-add as a one-liner.

Net: −28 lines (file shrinks from 235 to 207 lines including the
preserved bridge `measurable_shiftℤ` and downstream defs).

Author: cameronfreer

Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean

@@ -95,8 +95,9 @@ lemma eventuallyEq_comp_measurePreserving {f g : Ω[α] → ℝ}
   hT.quasiMeasurePreserving.ae_eq_comp hfg
 
 omit [MeasurableSpace α] [StandardBorelSpace α] in
-/-- General evaluation formula for shift iteration. -/
-lemma iterate_shift_eval' (k n : ℕ) (ω : Ω[α]) :
+/-- General evaluation formula for shift iteration. File-private — only caller
+is `iterate_shift_eval0'` directly below. -/
+private lemma iterate_shift_eval' (k n : ℕ) (ω : Ω[α]) :
     (shift^[k] ω) n = ω (k + n) := by
   induction k generalizing n with
   | zero => simp
@@ -107,8 +108,9 @@ lemma iterate_shift_eval' (k n : ℕ) (ω : Ω[α]) :
       ac_rfl
 
 omit [MeasurableSpace α] [StandardBorelSpace α] in
-/-- Evaluate the k-th shift at 0: shift^[k] ω 0 = ω k. -/
-lemma iterate_shift_eval0' (k : ℕ) (ω : Ω[α]) :
+/-- Evaluate the k-th shift at 0: shift^[k] ω 0 = ω k. File-private — only
+in-file caller. -/
+private lemma iterate_shift_eval0' (k : ℕ) (ω : Ω[α]) :
     (shift^[k] ω) 0 = ω k := by
   rw [iterate_shift_eval']
   simp

Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean

@@ -97,32 +97,12 @@ notation "Ωℤ[" α "]" => Ωℤ α
 /-- The two-sided shift on bi-infinite sequences. -/
 def shiftℤ (ω : Ωℤ[α]) : Ωℤ[α] := fun n => ω (n + 1)
 
-omit [MeasurableSpace α] in
-@[simp] lemma shiftℤ_apply (ω : Ωℤ[α]) (n : ℤ) :
-    shiftℤ (α := α) ω n = ω (n + 1) := rfl
-
 /-- The inverse shift on bi-infinite sequences. -/
 def shiftℤInv (ω : Ωℤ[α]) : Ωℤ[α] := fun n => ω (n - 1)
 
-omit [MeasurableSpace α] in
-@[simp] lemma shiftℤInv_apply (ω : Ωℤ[α]) (n : ℤ) :
-    shiftℤInv (α := α) ω n = ω (n - 1) := rfl
-
-omit [MeasurableSpace α] in
-@[simp] lemma shiftℤ_comp_shiftℤInv (ω : Ωℤ[α]) :
-    shiftℤ (α := α) (shiftℤInv (α := α) ω) = ω := by ext; simp [shiftℤ, shiftℤInv]
-
-omit [MeasurableSpace α] in
-@[simp] lemma shiftℤInv_comp_shiftℤ (ω : Ωℤ[α]) :
-    shiftℤInv (α := α) (shiftℤ (α := α) ω) = ω := by ext; simp [shiftℤ, shiftℤInv]
-
 /-- Restrict a bi-infinite path to its nonnegative coordinates. -/
 def restrictNonneg (ω : Ωℤ[α]) : Ω[α] := fun n => ω (Int.ofNat n)
 
-omit [MeasurableSpace α] in
-@[simp] lemma restrictNonneg_apply (ω : Ωℤ[α]) (n : ℕ) :
-    restrictNonneg (α := α) ω n = ω (Int.ofNat n) := rfl
-
 /-- Extend a one-sided path to the bi-infinite path space by duplicating the zeroth
 coordinate on the negative side. This is a convenient placeholder when we only need
 the right-infinite coordinates. -/
@@ -131,14 +111,6 @@ def extendByZero (ω : Ω[α]) : Ωℤ[α] :=
   | Int.ofNat n => ω n
   | Int.negSucc _ => ω 0
 
-omit [MeasurableSpace α] in
-@[simp] lemma restrictNonneg_extendByZero (ω : Ω[α]) :
-    restrictNonneg (α := α) (extendByZero (α := α) ω) = ω := by ext; simp [extendByZero]
-
-omit [MeasurableSpace α] in
-@[simp] lemma extendByZero_apply_nat (ω : Ω[α]) (n : ℕ) :
-    extendByZero (α := α) ω ↑n = ω n := by simp [extendByZero]
-
 @[measurability, fun_prop]
 lemma measurable_shiftℤ : Measurable (shiftℤ (α := α)) := by
   unfold shiftℤ; fun_prop

Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean

@@ -143,7 +143,7 @@ private lemma gRep_ae_eq_of_constant_orbit {g0 : Ω[α] → ℝ}
   exact gRep_eq_of_constant_orbit (g0 := g0) hω
 
 
-lemma ae_shift_invariance_on_rep
+private lemma ae_shift_invariance_on_rep
     {μ : Measure (Ω[α])} [IsProbabilityMeasure μ]
     (hσ : MeasurePreserving shift μ μ)
     {f g : Ω[α] → ℝ}

Exchangeability/Util/ProductBounds.lean

@@ -14,14 +14,14 @@ These are used in the contractability-based proof of de Finetti's theorem.
 
 ## Main results
 
-* `abs_prod_le_one`: |∏ f| ≤ 1 when all |f i| ≤ 1
 * `abs_prod_sub_prod_le`: |∏ f - ∏ g| ≤ ∑ |f_j - g_j| when factors bounded by 1
 -/
 
 namespace Exchangeability.Util
 
-/-- Helper: |∏ f| ≤ 1 when all |f i| ≤ 1. -/
-lemma abs_prod_le_one {n : ℕ} (f : Fin n → ℝ) (hf : ∀ i, |f i| ≤ 1) : |∏ i, f i| ≤ 1 := by
+/-- Helper: |∏ f| ≤ 1 when all |f i| ≤ 1. File-private — only caller is
+`abs_prod_sub_prod_le` directly below. -/
+private lemma abs_prod_le_one {n : ℕ} (f : Fin n → ℝ) (hf : ∀ i, |f i| ≤ 1) : |∏ i, f i| ≤ 1 := by
   rw [Finset.abs_prod]
   have h1 : ∏ i, |f i| ≤ ∏ _i : Fin n, (1 : ℝ) := by
     apply Finset.prod_le_prod