Section 6 — Induction Parameter Averaging Bounds

This file contains the uniform Jensen estimate used for averaged slice errors, together with the sliceConditioningLoss comparisons which replace the ambient factor m by m + 1 in the induction step.

References

• blueprint/src/chapter/ch10_induction.tex
• references/ldt-paper/inductive_step.tex

theorem MIPStarRE.LDT.MainInductionStep.avgOver_uniform_rpow_one_div_le_rpow_avg {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (f : α → Error) (n : ℕ) (hn : 1 ≤ n) (hf : ∀ (a : α), 0 ≤ f a) : (avgOver (uniformDistribution α) fun (a : α) => Real.rpow (f a) (1 / ↑n)) ≤ Real.rpow (avgOver (uniformDistribution α) f) (1 / ↑n)

Jensen's inequality for Real.rpow (1/n) against a uniform distribution: the average of (f a)^{1/n} is at most (average f)^{1/n}. This is the workhorse used inside each of the averaged-slice bounds (average_slice…_le) to push rpow (1/32) or rpow (1/1024) through a uniform avgOver on Fq params.

theorem MIPStarRE.LDT.MainInductionStep.m_mul_sliceConditioningLoss_rpow_le_next_m_mul_rpow (params : Parameters) {x c : Error} (hx : 0 ≤ x) (_hc_nonneg : 0 ≤ c) (hc_le_one : c ≤ 1) : ↑params.m * Real.rpow (sliceConditioningLoss params * x) c ≤ ↑params.next.m * Real.rpow x c

Internal helper: m · (sliceConditioningLoss · x)^c ≤ m_next · x^c for c ≤ 1.

Exposed for cross-module use in AvgSliceErrors.

theorem MIPStarRE.LDT.MainInductionStep.m_sq_mul_sliceConditioningLoss_rpow_le_next_sq_mul_rpow (params : Parameters) {x c : Error} (hx : 0 ≤ x) (hc_nonneg : 0 ≤ c) (hc_le_one : c ≤ 1) : ↑params.m ^ 2 * Real.rpow (sliceConditioningLoss params * x) c ≤ ↑params.next.m ^ 2 * Real.rpow x c

Internal helper: m² · (sliceConditioningLoss · x)^c ≤ m_next² · x^c for c ≤ 1.

Exposed for cross-module use in AvgSliceErrors.