refactor(DecisionTree,QueryComplexity): privatize 43 module-local proof helpers (#899)

Complexity/Computability/DecisionTree/CanonicalTree.lean

@@ -196,7 +196,7 @@ termination_by #ρ.free
 decreasing_by exact card_free_assign_lt h _
 
 /-- The query path depends only on the free bits of the input. -/
-theorem pathLength_congr {ρ : PartialAssignment ι} {x y : ι → Bool}
+private theorem pathLength_congr {ρ : PartialAssignment ι} {x y : ι → Bool}
     (h : ∀ i ∈ ρ.free, x i = y i) :
     F.pathLength ρ x = F.pathLength ρ y := by
   by_cases hq : F.queried ρ = []

Complexity/Computability/DecisionTree/Leaves.lean

@@ -159,7 +159,7 @@ def rank : DecisionTree ι β → ℕ
 theorem rank_leaf (b : β) : (leaf b : DecisionTree ι β).rank = 0 :=
   rfl
 
-theorem rank_node (i : ι) (left right : DecisionTree ι β) :
+private theorem rank_node (i : ι) (left right : DecisionTree ι β) :
     (node i left right).rank =
       if left.rank = right.rank then left.rank + 1 else max left.rank right.rank :=
   rfl
@@ -265,8 +265,8 @@ theorem IsDecisionList.rank_le_one {t : DecisionTree ι β} (h : t.IsDecisionLis
       split_ifs <;> omega
 
 /-- A decision list has at most `depth + 1` structural leaves. -/
-theorem IsDecisionList.leafCount_le_depth_add_one {t : DecisionTree ι β} (h : t.IsDecisionList) :
-    t.leafCount ≤ t.depth + 1 :=
+theorem IsDecisionList.leafCount_le_depth_add_one {t : DecisionTree ι β}
+    (h : t.IsDecisionList) : t.leafCount ≤ t.depth + 1 :=
   t.leafCount_le_depth_add_one_of_rank_le_one h.rank_le_one
 
 /-- A decision list has at most `depth` internal nodes. -/
@@ -294,7 +294,7 @@ def energy : DecisionTree ι β → ℕ
 theorem energy_leaf (b : β) : (leaf b : DecisionTree ι β).energy = 0 :=
   rfl
 
-theorem energy_node (i : ι) (left right : DecisionTree ι β) :
+private theorem energy_node (i : ι) (left right : DecisionTree ι β) :
     (node i left right).energy = max left.energy (right.energy + 1) :=
   rfl
 

Complexity/Computability/DecisionTree/Sensitivity.lean

@@ -75,13 +75,14 @@ theorem complexity_eq_card_of_forall_update_ne [Fintype ι] {f : (ι → Bool) 
 variable {n : ℕ}
 
 /-- The coordinates queried at an input certify the output of the tree. -/
-theorem isCertificate_queries {f : BooleanFunction n} {t : DecisionTree (Fin n) Bool}
+private theorem isCertificate_queries {f : BooleanFunction n} {t : DecisionTree (Fin n) Bool}
     (ht : t.Computes f) (x : BitString n) : IsCertificate f x (t.queries x) :=
   fun y hy => (ht y).symm.trans ((t.eval_eq_of_forall_mem_queries hy).trans (ht x))
 
 /-- Certificate complexity at an input is at most the depth of any tree computing the function. -/
-theorem certificateComplexityAt_le_depth {f : BooleanFunction n} {t : DecisionTree (Fin n) Bool}
-    (ht : t.Computes f) (x : BitString n) : certificateComplexityAt f x ≤ t.depth :=
+theorem certificateComplexityAt_le_depth {f : BooleanFunction n}
+    {t : DecisionTree (Fin n) Bool} (ht : t.Computes f) (x : BitString n) :
+    certificateComplexityAt f x ≤ t.depth :=
   (certificateComplexityAt_le (isCertificate_queries ht x)).trans (t.card_queries_le_depth x)
 
 /-- Certificate complexity is at most decision tree complexity. -/

Complexity/Computability/DecisionTree/Switching.lean

@@ -100,7 +100,7 @@ private theorem satisfying_of_mem (ht : (t.map Prod.fst).Nodup) {l : Literal ι}
     (t.stageCode x W).length = W.length := by
   induction W <;> simp_all [stageCode]
 
-theorem stageCode_eq_nil_iff {x : ι → Bool} {W : List ι} :
+private theorem stageCode_eq_nil_iff {x : ι → Bool} {W : List ι} :
     t.stageCode x W = [] ↔ W = [] := by
   cases W <;> simp [stageCode]
 

Complexity/Computability/QueryComplexity/Randomized.lean

@@ -163,19 +163,20 @@ theorem errorProb_nonneg : 0 ≤ μ.errorProb f x :=
 theorem errorProb_le_one : μ.errorProb f x ≤ 1 :=
   StdSimplex.sum_mul_le_of_forall_le fun _ _ => ite_le_one'
 
-theorem errorProb_eq_zero_iff : μ.errorProb f x = 0 ↔ ∀ t ∈ μ.weights.support, t.eval x = f x := by
+theorem errorProb_eq_zero_iff :
+    μ.errorProb f x = 0 ↔ ∀ t ∈ μ.weights.support, t.eval x = f x := by
   classical
   rw [errorProb, Finsupp.sum, Finset.sum_eq_zero_iff_of_nonneg fun t _ =>
     mul_nonneg (μ.weights_nonneg t) ite_nonneg']
   refine forall₂_congr fun t ht => ?_
   rw [mul_eq_zero, or_iff_right (Finsupp.mem_support_iff.mp ht)]
   split_ifs with h <;> simp [h]
 
-theorem errorProb_single_of_eq (h : t.eval x = f x) :
+private theorem errorProb_single_of_eq (h : t.eval x = f x) :
     errorProb (StdSimplex.single t : RandomizedDecisionTree ι β) f x = 0 := by
   simp [errorProb, h]
 
-theorem errorProb_single_of_ne (h : t.eval x ≠ f x) :
+private theorem errorProb_single_of_ne (h : t.eval x ≠ f x) :
     errorProb (StdSimplex.single t : RandomizedDecisionTree ι β) f x = 1 := by
   simp [errorProb, h]
 

Complexity/Computability/QueryComplexity/SensitivitySeparation/Internal/ProfileArithmetic.lean

@@ -56,7 +56,7 @@ def normalizedMax (M : ℝ) (n : ℕ) (s₀ s₁ : ℝ) : ℝ :=
   max (s₀ / M ^ n) (s₁ / M ^ (n + 1))
 
 /-- For `0 < M` and `0 ≤ s₀`, the normalized maximum is nonnegative. -/
-theorem normalizedMax_nonneg {M s₀ s₁ : ℝ} {n : ℕ}
+private theorem normalizedMax_nonneg {M s₀ s₁ : ℝ} {n : ℕ}
     (hM : 0 < M) (hs₀ : 0 ≤ s₀) : 0 ≤ normalizedMax M n s₀ s₁ :=
   (div_nonneg hs₀ (pow_pos hM n).le).trans (le_max_left _ _)
 

Complexity/Computability/QueryComplexity/SensitivitySeparation/Internal/RecursiveCandidates.lean

@@ -53,7 +53,7 @@ namespace Internal
 
 /-- For a target candidate `i`, the final predicate rejects the child of row `i` at the column
 `targetWitness F x hr i`. -/
-theorem targetWitness_false {k r h : ℕ} {I : Type} (T : Tournament k)
+private theorem targetWitness_false {k r h : ℕ} {I : Type} (T : Tournament k)
     (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool)
     (q : Fin h) (x : ((Fin k × Fin r) × I) → Bool) (hr : 0 < r) (i : Fin k)
     (hi : i ∈ targetCandidates T label F q x) :

Complexity/Computability/QueryComplexity/SensitivitySeparation/Internal/RecursiveFailures.lean

@@ -104,7 +104,7 @@ theorem targetFailures_empty_iff {k r h : ℕ} {I : Type}
 open scoped Classical in
 /-- A row `i` has no failed gate if and only if, for every outgoing neighbor `j` of `i`, the gate
 predicate `F (gateIndex q)` rejects the child `recursiveChild x j (label i j)`. -/
-theorem gateFailures_empty_iff {k r h : ℕ} {I : Type} (T : Tournament k)
+private theorem gateFailures_empty_iff {k r h : ℕ} {I : Type} (T : Tournament k)
     (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool)
     (q : Fin h) (x : ((Fin k × Fin r) × I) → Bool) (i : Fin k) :
     gateFailures T label F q x i = ∅ ↔

Complexity/Computability/QueryComplexity/Threshold.lean

@@ -88,8 +88,8 @@ theorem sensitivityAt_threshold_of_weight_eq {x : BitString n} (hx : weight x =
 
 /-- At an input of weight `j - 1`, for `j ≥ 1`, the sensitive coordinates of `Th^n_j` are its
 false bits. -/
-theorem sensitivityAt_threshold_of_weight_add_one_eq {x : BitString n} (hx : weight x + 1 = j) :
-    sensitivityAt (threshold n j) x = n + 1 - j := by
+theorem sensitivityAt_threshold_of_weight_add_one_eq {x : BitString n}
+    (hx : weight x + 1 = j) : sensitivityAt (threshold n j) x = n + 1 - j := by
   have : sensitiveCoords (threshold n j) x = univ.filter fun i => x i = false := by
     ext i
     have h : weight x ≠ j := by omega

Complexity/Computability/QueryComplexity/Yao.lean

@@ -80,7 +80,7 @@ theorem distributionalComplexity_le_depth (h : t.distributionalError ν f ≤ ε
   Nat.sInf_le ⟨t, h, le_rfl⟩
 
 /-- `D^ν_ε(f) = 0` for `ε < 0`, where no decision tree qualifies. -/
-theorem distributionalComplexity_of_neg (hε : ε < 0) : distributionalComplexity ε ν f = 0 :=
+private theorem distributionalComplexity_of_neg (hε : ε < 0) : distributionalComplexity ε ν f = 0 :=
   Nat.sInf_eq_zero.mpr <| Or.inr <| Set.eq_empty_of_forall_notMem fun _ ⟨_, h, _⟩ =>
     (not_le.mpr hε) (DecisionTree.distributionalError_nonneg.trans h)