OAI.IndependentProducts.main_gaussian_24

The theorem states that, for every real t>0, a lower bound holds for the averaged asymptotic midpoint modulus of a particular L1 span, and that the bound is strictly positive. The space is built from the tree of finite sequences of positive integers: one independent coordinate is attached to each nonroot vertex, each distributed as the law of the square of a standard real Gaussian (the pushforward of N(0,1) under x ↦ x²), and the infinite product measure is taken on the resulting sample space. The path product of a vertex multiplies the coordinates along the nonroot prefixes of its path, with the root giving the empty product 1. The space is the closed real linear span, inside L1 of the product measure, of all path products, equipped with its L1 norm. The averaged midpoint modulus at t takes the infimum over unit vectors x of the supremum, over closed finite-codimension subspaces F, of the infimum over y in F with norm at least 1 of (‖x+ty‖+‖x−ty‖)/2 − 1. With g(r) denoting the probability that a standard Gaussian satisfies |Z| ≥ r, the theorem asserts that this modulus is at least g(4√2(2+√2)/t)/8, and that g(4√2(2+√2)/t)/8 is greater than 0. The statement itself does not assume the multiplier-law hypotheses; the proof is admitted rather than verified here.