The Cramér n-letter change-of-measure predicate.

Captures the cylinder-n compatibility between Measure.infinitePi (fun _ => μ₀.tilted (lam * Y ·)) and (Measure.infinitePi μ₀).tilted (∑ lam * Y ∘ eval i), in the form usable as input to Cramér's lower-bound change-of-measure step.

The intended interpretation: for every n and every measurable event E ⊆ {ω | a·n ≤ ∑ i ∈ Finset.range n, Y (ω i)}, the un-tilted product measure of E admits the Chernoff-style lower bound exp(-n · (lam · a − Λ(lam))) · μ_tilt(E) − o(1) ≤ μ.real E, where μ_tilt := Measure.infinitePi (fun _ => μ₀.tilted (lam * Y ·)) and Λ := cgf Y μ₀. This is the textbook density identity (dμ_tilt / dμ)|_{cylinder n} = exp(lam · ∑ Y(ω_i) − n·Λ(lam)).

The cylinder lift: an event over the first n coordinates of the infinite product, expressed via a predicate on the partial sum, has infinitePi mass equal to the corresponding Measure.pi (Fin n) mass. Works for any constant factor ν (apply with ν = μ₀ and ν = μ₀.tilted ...).

The finite change-of-measure lower bound (Measure.pi level).

For lam ≥ 0, on the window W_n := {x | a·n ≤ ∑ Y(x i) < (a+ε)·n} the un-tilted product mass of the half-line event E_n := {x | a·n ≤ ∑ Y(x i)} is bounded below by exp(-n·(lam·a − Λ + lam·ε)) times the tilted product mass of W_n, where Λ = cgf Y μ₀ lam. The density d(pi μ₀)/d(pi μ_tilt) is exp(−lam·∑Y + n·Λ), bounded below on W_n by exp(−lam(a+ε)n + nΛ).

@audit:ok (genuine density-bound proof)

The residual predicate: the tilted infinite-product window mass is eventually at least 1/2. It holds precisely when the tilted mean ∫ Y ∂μ₀.tilted lies in the window [a, a+ε), which is the Cramér optimality condition ∫ Y ∂μ₀.tilted = a.

See also tilted_lln_in_probability_real.

The residual reduction: the residual window predicate implies the full n-letter RN-deriv predicate IsMeasureInfinitePiTiltedEq.

@audit:ok (h_res is genuinely consumed (filter_upwards [h_res a ε hε]) to supply the window-mass input, not a vacuous bundle.)

The per-instance tilted window mass tends to 1 (interior case).

The ∀a∀ε predicate IsTiltedWindowEventuallyLarge is false in general (for a far from the tilted mean the window has vanishing mass). The meaningful statement is the per-instance one: when the tilted mean m := ∫ Y ∂(μ₀.tilted (lam·Y)) lies strictly inside the window (a, a+ε), the tilted infinite-product mass of {ω | a·n ≤ ∑_{i<n} Y(ω i) < (a+ε)·n} tends to 1.

The per-instance tilted window mass is eventually ≥ 1/2 (interior case). This is the per-instance replacement for the (generally false) ∀a∀ε IsTiltedWindowEventuallyLarge predicate.

See also tiltedWindow_eventually_tendsto_one.

The tilted mean equals the cgf derivative (cgf-derivative bridge).

For a bounded measurable Y under a probability measure μ₀, the tilted mean ∫ Y ∂(μ₀.tilted (lam·Y)) equals the first derivative of the cgf at lam: ∫ ω, Y ω ∂(μ₀.tilted (fun ω => lam * Y ω)) = deriv (cgf Y μ₀) lam.

The interior side condition lam ∈ interior (integrableExpSet Y μ₀) holds because boundedness of Y makes exp (t·Y) integrable for every t, so integrableExpSet Y μ₀ = Set.univ and its interior is again Set.univ.

@audit:ok