Sensitivity separation: labeling estimate

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/LabelingEstimate.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_union_bound_numerator {M r : ℕ} (hM : 3 ≤ M) (hMr : M ≤ r ^ 2) : (2 * M ^ 2 + 1) ^ 16 * M ^ 20 ≤ 3 ^ 16 * r ^ 104

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_union_bound_constant {M : ℕ} (hM : 3 ≤ M) : 3 ^ 16 < M ^ 20

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_power_bound {M r : ℕ} (hM : 3 ≤ M) (hMr : M ≤ r ^ 2) : (2 * M ^ 2 + 1) ^ 16 < r ^ 104

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_union_bound_real {M r : ℕ} (hM : 3 ≤ M) (hMr : M ≤ r ^ 2) : ↑((2 * M ^ 2 + 1) ^ 16) / ↑r ^ 104 ≤ 3 ^ 16 / ↑M ^ 20 ∧ 3 ^ 16 / ↑M ^ 20 < 1

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_sqrt_expression {M : ℕ} (hM : 0 < M) : (3 * ↑M ^ 2) ^ 16 / √↑M ^ 104 = 3 ^ 16 / ↑M ^ 20

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.labeling_source_estimate {M : ℕ} (hM : 3 ≤ M) : ↑((2 * M ^ 2 + 1) ^ 16) / ↑⌈√↑M⌉₊ ^ 104 ≤ (3 * ↑M ^ 2) ^ 16 / √↑M ^ 104 ∧ (3 * ↑M ^ 2) ^ 16 / √↑M ^ 104 = 3 ^ 16 / ↑M ^ 20 ∧ 3 ^ 16 / ↑M ^ 20 < 1