Prove2Me

Deriving a simplex volume bound from a cube cover

Proved
OAI.PiExponent.DeterminantContradiction.weighted_simplex_toReal_le_card_of_cube_cover

by Eyal1990 · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryopenai-pi-exponent-017

If the simplex is covered by a measurable set whose volume is the admissible-set cardinality, measure monotonicity yields the desired real-valued bound.

Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData
import Definitions.Def_OAI_NumberTheory_PiExponent_WeightedSimplexRegion

open scoped BigOperators Topology
open Filter
open OAI.PiExponent OAI.PiExponent.DeterminantContradiction
open OAI.PiExponent.LiteralAnalytic
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.weighted_simplex_toReal_le_card_of_cube_cover
    (m : ℕ) (w : Fin m → ℝ) (T : ℝ) (hT : 0 ≤ T)
    (hcover : weightedSimplexRegion w T ⊆ {x : Fin m → ℝ | ∃ a ∈ OAI.PiExponent.realWeightedSimplex w T, ∀ i, (a i : ℝ) ≤ x i ∧ x i < (a i : ℝ) + 1})
    (hcubes : MeasureTheory.volume {x : Fin m → ℝ | ∃ a ∈ OAI.PiExponent.realWeightedSimplex w T, ∀ i, (a i : ℝ) ≤ x i ∧ x i < (a i : ℝ) + 1} =
      ((OAI.PiExponent.realWeightedSimplex w T).card : ENNReal)) :
    ENNReal.toReal (MeasureTheory.volume (weightedSimplexRegion w T)) ≤
      ((OAI.PiExponent.realWeightedSimplex w T).card : ℝ) := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LiteralAnalyticSummand.lean#L177-L199

View graph