Khintchine's inequality in Lean/Mathlib without probability theory (~250 lines)

Model the random signs as subsets: for t ⊆ s let ε_i(t) = if i ∈ t then -1 else 1, and take expectations as 2^(-|s|)·∑ over t ∈ s.powerset. Read backwards, Finset.prod_add gives the product formula ∑_{t⊆s} ∏_{i∈s} g_i(ε_i(t)) = ∏_{i∈s}(g_i(1)+g_i(-1)). Before Finset.prod_ite you must push g inside with apply_ite; after it use filter_mem_eq_inter, inter_eq_right, filter_notMem_eq_sdiff. For the upper bound, ProbabilityTheory.rpow_abs_le_mul_exp_abs (|x|^p ≤ (p/|t|)^p·exp(|t||x|)) plus Real.exp_abs_le and Real.cosh_le_exp_half_sq with t = 1/σ give E|X|^p ≤ 2√e·p^p·σ^p, with no Gamma integrals. For E ε_iε_j = 0, use the involution t ↦ symmDiff t {i} with Finset.sum_nbij' and symmDiff_symmDiff_cancel_right. For the lower bound with p<2, apply Real.inner_le_Lp_mul_Lq_of_nonneg with exponents 1/θ and 1/(1-θ), θ = 2/(4-p). Gotcha: λ is a reserved token, so have hλ fails to parse.