Additional L² Helpers and Incomplete Lemmas #
This file contains technical lemmas and placeholder definitions that support
the L² proof of de Finetti's theorem. Some lemmas have sorry placeholders
that will eventually be replaced with proper proofs from mathlib or local implementations.
Contents #
- Elementary helpers (clip01, Lipschitz properties)
- L¹ convergence helpers
- Boundedness helpers
- AE strong measurability helpers
- Deep results requiring further work (marked with sorry)
Note #
The incomplete lemmas in this file are placeholders for complex proofs that are deferred to allow the main proof structure to be complete. Each sorry can be replaced with a proper proof.
Forward declarations and placeholders #
This section contains forward declarations and placeholder definitions for deep results. Each sorry can be replaced with a proper proof from mathlib or a local implementation.
CDF limits at ±∞: F(t) → 0 as t → -∞ and F(t) → 1 as t → +∞.
This is now trivial because cdf_from_alpha is defined via stieltjesOfMeasurableRat,
which guarantees these limits for ALL ω (not just a.e.) by construction.
The stieltjesOfMeasurableRat construction automatically patches the null set where
the raw L¹ limit alphaIic would fail to have proper CDF limits.
L¹ Convergence Helpers #
Boundedness Helpers #
AE Strong Measurability for iInf/iSup #
For each fixed t, ω ↦ ν(ω)((-∞,t]) is measurable. This is the base case for the π-λ theorem.
For each measurable set s, the map ω ↦ ν(ω)(s) is measurable.
This is the key measurability property needed for complete_from_directing_measure. Uses monotone class theorem (π-λ theorem) - prove for intervals, extend to all Borel sets.
L¹ Limit Uniqueness #
The following lemma establishes that L¹ limits are unique up to a.e. equality. This is used to prove the linearity lemmas below.
If a sequence converges in L¹ to two limits, they are a.e. equal.
This follows from the triangle inequality: ‖g - h‖₁ ≤ ‖g - f_n‖₁ + ‖f_n - h‖₁, and both terms go to 0.
Linearity of L¹ Limits #
The following lemmas establish that the L¹ limit functional from weighted_sums_converge_L1
is linear: if f and g have L¹ limits α_f and α_g, then f + g has limit α_f + α_g,
and c * f has limit c * α_f.
These are essential for the functional monotone class argument that extends from indicators of half-lines to all bounded measurable functions.
Scalar multiplication of L¹ limits: if f has L¹ limit α, then cf has L¹ limit cα.
Addition of L¹ limits: if f has limit α_f and g has limit α_g, then f+g has limit α_f + α_g.
Subtraction/complement: L¹ limit of (1 - f) is (1 - limit of f).
This is used for the complement step in the π-λ argument: 1_{Sᶜ} = 1 - 1_S, so the limit for the complement is 1 minus the limit for the set.
The L¹ limit of the constant function 1 is 1 a.e.
This is immediate since the Cesàro average of constant 1 is exactly 1: (1/N) Σ_k 1 = (1/N) * N = 1.
The directing measure integrates to give α_f.
For any bounded measurable f, we have α_f(ω) = ∫ f dν(ω) a.e. This is the fundamental bridge property.
Packaged directing measure theorem: Existence of a directing kernel with all key properties bundled together.
For a contractable sequence X on ℝ, there exists:
- A limit function α ∈ L¹ that is the L¹ limit of Cesàro averages
- A random probability measure ν(·) on ℝ (the directing measure)
- The identification α = ∫ f dν a.e.
This packages the outputs of directing_measure and directing_measure_integral
into a single existential statement that is convenient for applications.
Proof: Follows directly from directing_measure_integral which provides
the limit α and its identification with ∫ f dν, combined with
directing_measure_isProbabilityMeasure and directing_measure_measurable.
The integral of alphaIic equals the marginal probability.
By the L¹ convergence property of the Cesàro averages and contractability (which implies all marginals are equal), we have: ∫ alphaIic(t, ω) dμ = μ(X_0 ∈ Iic t)
This is a key step in proving the bridge property.
Proof outline:
- alphaIic is the clipped L¹ limit of Cesàro averages of 1_{Iic t}(X_i)
- By L¹ convergence: ∫ (limit) dμ = lim ∫ (Cesàro average) dμ
- By contractability: each μ(X_i ∈ Iic t) = μ(X_0 ∈ Iic t)
- Therefore: ∫ alphaIic dμ = μ(X_0 ∈ Iic t)
Injective to StrictMono via Sorting #
For the bridge property, we need to convert an injective function k : Fin m → ℕ
to a strictly monotone one. This is done by sorting the image of k.
Note: The lemma injective_implies_strictMono_perm is now in
Exchangeability.Util.StrictMono and imported via open at the top of this file.
Collision Bound for Route B #
The key estimate for Route B: the fraction of non-injective maps φ : Fin m → Fin N tends to 0 as N → ∞, with rate O(m²/N).
Bijection between constrained functions {φ | φ i = φ j} and functions on Fin n.
The constraint φ i = φ j means φ j is determined by φ i, so effectively we only need to specify φ on {k | k ≠ j}, which has cardinality n when the domain is Fin (n+1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The number of collision pairs is at most m².
The number of non-injective maps φ : Fin m → Fin N is at most m² * N^(m-1).
Proof: A non-injective map has some pair (i, j) with i ≠ j and φ(i) = φ(j). By union bound over the m² pairs, and for each pair there are at most N^(m-1) maps.
The fraction of non-injective maps tends to 0 as N → ∞.
For fixed m, the fraction (# non-injective) / N^m ≤ m²/N → 0.
Product L¹ Convergence #
For Route B, we need: if each factor converges in L¹, then the product converges in L¹ (under boundedness assumptions).
Product of L¹-convergent bounded sequences converges in L¹.
If f_n(i) → g(i) in L¹ for each i, and all functions are bounded by 1, then ∏_i f_n(i) → ∏_i g(i) in L¹.
Proof: By abs_prod_sub_prod_le, we have pointwise:
|∏_i f_n(i) - ∏_i g(i)| ≤ ∑_j |f_n(j) - g(j)|
Integrating and using Fubini: ∫ |∏ f - ∏ g| ≤ ∫ ∑_j |f_j - g_j| = ∑_j ∫ |f_j - g_j|
The RHS tends to 0 by h_conv and tendsto_finset_sum.
Block index function is strictly monotone.
For the block-separated approach, we define indices using disjoint ordered blocks: k_φ(i) := i * N + φ(i) for φ : Fin m → Fin N
This is STRICTLY MONOTONE for any φ because: k_φ(i) = i * N + φ(i) ≤ i * N + (N-1) < (i+1) * N ≤ k_φ(i+1)
This is the key insight that makes the block-separated approach work: every selection is StrictMono, so contractability applies to EVERY term (no exchangeability required).
The bridge property: E[∏ᵢ 𝟙_{Bᵢ}(X_{k(i)})] = E[∏ᵢ ν(·)(Bᵢ)].
This is the key property needed for complete_from_directing_measure.
Uses indicator_product_bridge from BridgeProperty.lean, establishing that
the directing measure satisfies hν_law via shift invariance of conditional expectations.
Original proof structure (commented out due to incomplete lemmas) #
The original proof attempted to show:
- Reduce injective k to strictly monotone via permutation
- Use contractability for distributional equality
- Apply U-statistic expansion for product expectations
- Conclude via L¹ convergence of block averages
Key intermediate lemmas that need completion:
- h_pblock_vs_shifted: Bound on shifted averages
- h_L1_shifted_ref: L¹ bound from L² via Cauchy-Schwarz
- h_block_L1: Product L¹ convergence
Main packaging theorem for L² proof.
This theorem packages all the directing measure properties needed by
CommonEnding.complete_from_directing_measure:
νis a probability measure for all ωω ↦ ν(ω)(s)is measurable for all measurable sets s- The bridge property: E[∏ᵢ 1_{Bᵢ}(X_{k(i)})] = E[∏ᵢ ν(·)(Bᵢ)]
This enables the final step of the L² proof of de Finetti's theorem.