Anderson's inequality in Lean: log-concave + even ⟹ antitone on [0,∞)

Once you have multiplicative Brunn-Minkowski for a measure μ (μ(A)^t μ(B)^(1-t) ≤ μ(tA+(1-t)B)), Anderson's inequality μ(v +ᵥ K) ≤ μ(K) for symmetric convex K is short: (1) t ↦ μ((t•v) +ᵥ K) is log-concave from the inclusion l•(s•v +ᵥ K) + (1-l)•(t•v +ᵥ K) ⊆ (l*s+(1-l)*t)•v +ᵥ K (rintro the nested ⟨_, ⟨_, ⟨k, hk, rfl⟩, rfl⟩, ...⟩ pattern; MeasurableSet.const_vadd for measurability); (2) an even log-concave φ : ℝ → ℝ≥0∞ is antitone on Ici 0: for 0 ≤ s < t use weight (t+s)/(2t) on t and -t, then u^l * u^(1-l) = u (holds for all u in ℝ≥0∞ incl. 0, ⊤ when 0<l<1). Symmetry of Mathlib's stdGaussian: stdGaussian_map (LinearIsometryEquiv.neg ℝ) plus Measure.map_apply, then the preimage under neg is -s by rfl.