MaxLeafFormal.MLSNec

Source file MaxLeafFormal/MLSNec.lean of the Lean project (how it is built).

Statements of the paper formalised here: Lemma 3.9, Proposition 3.10.

import MaxLeafFormal.MLS

/-!
# General results of the framework used by `prop:fa-pd-tight`

The second inequality of `lem:fw-gf` (pointwise form, with its two proof steps), the null-set
step of the model (`trialMeasure_card_null`) and `prop:fw-necessary` in probability form.
-/
namespace MaxLeafFormal.MLSNec
open Finset MaxLeafFormal.MLS
variable {U : Type*} [Fintype U] [DecidableEq U]

/-- One term of `W_S`: `μ_t(S) y^t ≤ W_S(y)` for `y ≥ 0` (proof of `lem:fw-gf`). -/
theorem mu_mul_pow_le_W (g : Finset U → ℕ → ℝ) (S : Finset U) (k t : ℕ) (y : ℝ) (hy : 0 ≤ y) :
    mu g S k t * y ^ t ≤ W g S k y := by
  unfold MLS.mu MLS.W
  rw [sum_mul]
  calc ∑ X ∈ S.powersetCard t, (2:ℝ) ^ (-(g X (k - t))) * y ^ t
      = ∑ X ∈ S.powersetCard t, y ^ X.card * (2:ℝ) ^ (-(g X (k - X.card))) := by
        refine sum_congr rfl fun X hX => ?_
        rw [(mem_powersetCard.1 hX).2, mul_comm]
    _ ≤ ∑ X ∈ S.powerset, y ^ X.card * (2:ℝ) ^ (-(g X (k - X.card))) := by
        apply sum_le_sum_of_subset_of_nonneg
        · intro X hX
          exact mem_powerset.2 (mem_powersetCard.1 hX).1
        · intro X _ _
          exact mul_nonneg (pow_nonneg hy _) (Real.rpow_nonneg (by norm_num) _)

/-- `C(n,t) y^t ≥ (1+y)^n / (n+1)` at `y = t/(n-t)`, for `t < n` (proof of `lem:fw-gf`). -/
theorem pow_le_choose_mul (n t : ℕ) (ht : t < n) :
    (1 + (t : ℝ) / ((n : ℝ) - t)) ^ n
      ≤ ((n : ℝ) + 1) * (n.choose t : ℝ) * ((t : ℝ) / ((n : ℝ) - t)) ^ t := by
  have htn : (t : ℝ) < n := by exact_mod_cast ht
  have hnt : (0 : ℝ) < (n : ℝ) - t := by linarith
  have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n
  generalize hy : (t : ℝ) / ((n : ℝ) - t) = y
  have hy0 : 0 ≤ y := hy ▸ div_nonneg (Nat.cast_nonneg _) hnt.le
  have hyb : y * ((n : ℝ) - t) = t := by rw [← hy]; exact div_mul_cancel₀ _ hnt.ne'
  -- the ratio of consecutive terms
  have hrat : ∀ s, s < n → (n.choose (s + 1) : ℝ) * y ^ (s + 1) * (((s : ℝ) + 1) * ((n : ℝ) - t))
      = (n.choose s : ℝ) * y ^ s * (((n : ℝ) - s) * t) := by
    intro s hs
    have h' : (n.choose (s + 1) : ℝ) * ((s : ℝ) + 1) = (n.choose s : ℝ) * ((n : ℝ) - s) := by
      have h2 : ((n.choose (s + 1) * (s + 1) : ℕ) : ℝ) = ((n.choose s * (n - s) : ℕ) : ℝ) := by
        rw [Nat.choose_succ_right_eq]
      push_cast [Nat.cast_sub hs.le] at h2
      exact h2
    calc (n.choose (s + 1) : ℝ) * y ^ (s + 1) * (((s : ℝ) + 1) * ((n : ℝ) - t))
        = ((n.choose (s + 1) : ℝ) * ((s : ℝ) + 1)) * y ^ s * (y * ((n : ℝ) - t)) := by ring
      _ = (n.choose s : ℝ) * y ^ s * (((n : ℝ) - s) * t) := by rw [h', hyb]; ring
  have hup : ∀ s, s < t → (n.choose s : ℝ) * y ^ s ≤ (n.choose (s + 1) : ℝ) * y ^ (s + 1) := by
    intro s hs
    have hs' : (s : ℝ) + 1 ≤ t := by exact_mod_cast hs
    have hpos : (0 : ℝ) < ((s : ℝ) + 1) * ((n : ℝ) - t) := mul_pos (by positivity) hnt
    have hst : ((s : ℝ) + 1) * ((n : ℝ) - t) ≤ ((n : ℝ) - s) * t := by
      nlinarith [mul_nonneg hn0 (by linarith : (0 : ℝ) ≤ t - s - 1)]
    have hf0 : 0 ≤ (n.choose s : ℝ) * y ^ s := mul_nonneg (Nat.cast_nonneg _) (pow_nonneg hy0 _)
    refine le_of_mul_le_mul_right ?_ hpos
    rw [hrat s (by omega)]
    exact mul_le_mul_of_nonneg_left hst hf0
  have hdown : ∀ s, t ≤ s → s < n →
      (n.choose (s + 1) : ℝ) * y ^ (s + 1) ≤ (n.choose s : ℝ) * y ^ s := by
    intro s hs hsn
    have hs1 : (t : ℝ) ≤ s := by exact_mod_cast hs
    have hpos : (0 : ℝ) < ((s : ℝ) + 1) * ((n : ℝ) - t) := mul_pos (by positivity) hnt
    have hst : ((n : ℝ) - s) * t ≤ ((s : ℝ) + 1) * ((n : ℝ) - t) := by
      nlinarith [mul_nonneg hn0 (by linarith : (0 : ℝ) ≤ s - t)]
    have hf0 : 0 ≤ (n.choose s : ℝ) * y ^ s := mul_nonneg (Nat.cast_nonneg _) (pow_nonneg hy0 _)
    refine le_of_mul_le_mul_right ?_ hpos
    rw [hrat s hsn]
    exact mul_le_mul_of_nonneg_left hst hf0
  have hle_up : ∀ d s, s + d = t → (n.choose s : ℝ) * y ^ s ≤ (n.choose t : ℝ) * y ^ t := by
    intro d
    induction d with
    | zero => intro s hs; rw [Nat.add_zero] at hs; subst hs; exact le_rfl
    | succ d ih => intro s hs; exact (hup s (by omega)).trans (ih (s + 1) (by omega))
  have hle_down : ∀ d, t + d ≤ n →
      (n.choose (t + d) : ℝ) * y ^ (t + d) ≤ (n.choose t : ℝ) * y ^ t := by
    intro d
    induction d with
    | zero => intro _; simp only [Nat.add_zero, le_refl]
    | succ d ih =>
      intro hd
      exact (hdown (t + d) (by omega) (by omega)).trans (ih (by omega))
  have hbound : ∀ s, s ≤ n → (n.choose s : ℝ) * y ^ s ≤ (n.choose t : ℝ) * y ^ t := by
    intro s hs
    rcases Nat.lt_or_ge s t with h | h
    · exact hle_up (t - s) s (by omega)
    · have := hle_down (s - t) (by omega)
      rwa [show t + (s - t) = s by omega] at this
  have hsum : (1 + y) ^ n = ∑ s ∈ range (n + 1), (n.choose s : ℝ) * y ^ s := by
    rw [add_comm (1 : ℝ) y, add_pow]
    refine sum_congr rfl fun s _ => ?_
    rw [one_pow, mul_one, mul_comm]
  rw [hsum]
  calc ∑ s ∈ range (n + 1), (n.choose s : ℝ) * y ^ s
      ≤ ∑ _s ∈ range (n + 1), (n.choose t : ℝ) * y ^ t :=
        sum_le_sum fun s hs => hbound s (Nat.lt_succ_iff.1 (mem_range.1 hs))
    _ = ((n : ℝ) + 1) * (n.choose t : ℝ) * y ^ t := by
        rw [sum_const, card_range, nsmul_eq_mul]; push_cast; ring

namespace Aux

theorem mu_nonneg (g : Finset U → ℕ → ℝ) (S : Finset U) (k t : ℕ) : 0 ≤ mu g S k t :=
  sum_nonneg fun _ _ => Real.rpow_nonneg (by norm_num) _

theorem W_nonneg (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (y : ℝ) (hy : 0 ≤ y) :
    0 ≤ W g S k y :=
  sum_nonneg fun _ _ => mul_nonneg (pow_nonneg hy _) (Real.rpow_nonneg (by norm_num) _)

/-- `(1+n)^n ≤ (n+1) n^n` (the case `t = n` of `lem:fw-gf`). -/
theorem one_add_pow_le (n : ℕ) : (1 + (n : ℝ)) ^ n ≤ ((n : ℝ) + 1) * (n : ℝ) ^ n := by
  have hsum : (1 + (n : ℝ)) ^ n = ∑ s ∈ range (n + 1), (n.choose s : ℝ) * (n : ℝ) ^ s := by
    rw [add_comm (1 : ℝ) _, add_pow]
    refine sum_congr rfl fun s _ => ?_
    rw [one_pow, mul_one, mul_comm]
  have hterm : ∀ s ∈ range (n + 1), (n.choose s : ℝ) * (n : ℝ) ^ s ≤ (n : ℝ) ^ n := by
    intro s hs
    have hsn : s ≤ n := Nat.lt_succ_iff.1 (mem_range.1 hs)
    have hc : n.choose s ≤ n ^ (n - s) := by
      rw [← Nat.choose_symm hsn]
      exact Nat.choose_le_pow n (n - s)
    have hc' : (n.choose s : ℝ) ≤ (n : ℝ) ^ (n - s) := by exact_mod_cast hc
    calc (n.choose s : ℝ) * (n : ℝ) ^ s ≤ (n : ℝ) ^ (n - s) * (n : ℝ) ^ s :=
          mul_le_mul_of_nonneg_right hc' (by positivity)
      _ = (n : ℝ) ^ n := by rw [← pow_add, Nat.sub_add_cancel hsn]
  rw [hsum]
  calc ∑ s ∈ range (n + 1), (n.choose s : ℝ) * (n : ℝ) ^ s
      ≤ ∑ _s ∈ range (n + 1), (n : ℝ) ^ n := sum_le_sum hterm
    _ = ((n : ℝ) + 1) * (n : ℝ) ^ n := by
        rw [sum_const, card_range, nsmul_eq_mul]; push_cast; ring

end Aux

/-- `lem:fw-gf`, second inequality, in the pointwise form of its proof:
for each sample size `t ≤ k` some `y ≥ 0` has `(1+y)^n / W_S(y) ≤ (n+1) · C(n,t) / μ_t(S)`. -/
theorem fw_gf_upper (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ) (hSk : S.card = k)
    (t : ℕ) (ht : t ≤ k) :
    ∃ y : ℝ, 0 ≤ y ∧
      mu g S k t * (1 + y) ^ Fintype.card U
        ≤ ((Fintype.card U : ℝ) + 1) * ((Fintype.card U).choose t : ℝ) * W g S k y := by
  set n := Fintype.card U with hn
  have htn : t ≤ n := ht.trans (hSk ▸ card_le_univ S)
  have hmu0 := Aux.mu_nonneg g S k t
  rcases Nat.eq_zero_or_pos t with h0 | hpos
  · -- `t = 0`: `y = 0`
    subst h0
    refine ⟨0, le_rfl, ?_⟩
    have h1 := mu_mul_pow_le_W g S k 0 0 le_rfl
    have hW0 := Aux.W_nonneg g S k 0 le_rfl
    rw [pow_zero, mul_one] at h1
    rw [add_zero, one_pow, mul_one, Nat.choose_zero_right, Nat.cast_one, mul_one]
    nlinarith
  rcases lt_or_eq_of_le htn with hlt | heq
  · -- `0 < t < n`: `y = t/(n-t)`
    have hnt : (0 : ℝ) < (n : ℝ) - t := by
      have : (t : ℝ) < n := by exact_mod_cast hlt
      linarith
    refine ⟨(t : ℝ) / ((n : ℝ) - t), div_nonneg (Nat.cast_nonneg _) hnt.le, ?_⟩
    have h1 := mu_mul_pow_le_W g S k t _ (div_nonneg (Nat.cast_nonneg t) hnt.le)
    have h2 := pow_le_choose_mul n t hlt
    have hc0 : (0 : ℝ) ≤ ((n : ℝ) + 1) * (n.choose t : ℝ) := by positivity
    calc mu g S k t * (1 + (t : ℝ) / ((n : ℝ) - t)) ^ n
        ≤ mu g S k t * (((n : ℝ) + 1) * (n.choose t : ℝ) * ((t : ℝ) / ((n : ℝ) - t)) ^ t) :=
          mul_le_mul_of_nonneg_left h2 hmu0
      _ = ((n : ℝ) + 1) * (n.choose t : ℝ) * (mu g S k t * ((t : ℝ) / ((n : ℝ) - t)) ^ t) := by
          ring
      _ ≤ ((n : ℝ) + 1) * (n.choose t : ℝ) * W g S k ((t : ℝ) / ((n : ℝ) - t)) :=
          mul_le_mul_of_nonneg_left h1 hc0
  · -- `t = n`: `y = n`
    rw [heq] at hmu0 ⊢
    refine ⟨(n : ℝ), Nat.cast_nonneg _, ?_⟩
    have h1 := mu_mul_pow_le_W g S k n (n : ℝ) (Nat.cast_nonneg _)
    have h2 := Aux.one_add_pow_le n
    rw [Nat.choose_self, Nat.cast_one, mul_one]
    calc mu g S k n * (1 + (n : ℝ)) ^ n ≤ mu g S k n * (((n : ℝ) + 1) * (n : ℝ) ^ n) :=
          mul_le_mul_of_nonneg_left h2 hmu0
      _ = ((n : ℝ) + 1) * (mu g S k n * (n : ℝ) ^ n) := by ring
      _ ≤ ((n : ℝ) + 1) * W g S k (n : ℝ) := mul_le_mul_of_nonneg_left h1 (by positivity)

/-- The samples have their nominal sizes almost surely: under `trialMeasure`, the outcomes in
which some slot `j = ((t, θ), r)` has a sample with other than `t` elements form a null set
(`alg:fw-mls`, step 1). -/
theorem trialMeasure_card_null (k : ℕ) (ψ Γ κ : ℝ) :
    trialMeasure (U := U) k ψ Γ κ {o | ∃ j, (o j).card ≠ (j.1.1 : ℕ)} = 0 := by
  have hset : {o : Slot (Fintype.card U) k ψ Γ κ → Finset U | ∃ j, (o j).card ≠ (j.1.1 : ℕ)}
      = ⋃ j, Function.eval j ⁻¹' {X : Finset U | X.card ≠ (j.1.1 : ℕ)} := by
    ext o; simp
  rw [hset]
  refine MeasureTheory.measure_iUnion_null fun j => ?_
  unfold trialMeasure
  haveI : ∀ j : Slot (Fintype.card U) k ψ Γ κ, MeasureTheory.IsFiniteMeasure
      (ProbabilityTheory.uniformOn ((powersetCard (j.1.1 : ℕ) (univ : Finset U) :
        Finset (Finset U)) : Set (Finset U))) := fun j => by
    unfold ProbabilityTheory.uniformOn; infer_instance
  apply MeasureTheory.Measure.pi_eval_preimage_null
  rw [ProbabilityTheory.uniformOn_eq_zero_iff (Finset.finite_toSet _)]
  ext X
  simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Finset.mem_coe, Set.mem_empty_iff_false,
    iff_false, not_and]
  intro hX h
  exact h (mem_powersetCard.1 hX).2

/-- `P_nec` of `prop:fw-necessary`, for the cap `MLS.cap`. -/
noncomputable def Pnec (n k : ℕ) (ψ Γ κ : ℝ) : ℝ :=
  8 * Γ * ((k : ℝ) + 1) * ((cap n ψ Γ : ℝ) + 1) * (κ * ((cap n ψ Γ : ℝ) + 1) + 1)

/-- `prop:fw-necessary`, probability form: the probability that some trial of MLS
on `(I,k)` runs the extension on a subset of `S` is at most
`P_nec · 2^{ψn} · B`, for every bound `B ≥ max_{t ≤ |S|} μ^{(k)}_t(S)/C(n,t)`. -/
theorem mls_necessary (g : Finset U → ℕ → ℝ) (k : ℕ) (hk : k ≤ Fintype.card U)
    (ψ Γ κ : ℝ) (hψ : 0 ≤ ψ) (hΓ : 1 ≤ Γ) (hκ : 0 < κ)
    (S : Finset U) (hSk : S.card ≤ k) (B : ℝ)
    (hB : ∀ t ≤ S.card, mu g S k t / ((Fintype.card U).choose t : ℝ) ≤ B) :
    (trialMeasure k ψ Γ κ
        {o | ∃ j, o j ⊆ S ∧ g (o j) (k - j.1.1) ≤ ((j.1.2 : ℕ) : ℝ)}).toReal
      ≤ Pnec (Fintype.card U) k ψ Γ κ * (2:ℝ) ^ (ψ * Fintype.card U) * B := by
  classical
  set n := Fintype.card U with hn
  set Θ := cap n ψ Γ with hΘ
  have hfac := trialMeasure_factor_prob (U := U) k hk ψ Γ κ
  set μ := trialMeasure (U := U) k ψ Γ κ with hμ
  haveI : MeasureTheory.IsProbabilityMeasure μ := by
    rw [hμ]; unfold trialMeasure
    have := hfac
    infer_instance
  -- `B ≥ 0`
  have hB0 : 0 ≤ B := by
    have := hB 0 (Nat.zero_le _)
    exact le_trans (div_nonneg (Aux.mu_nonneg g S k 0) (Nat.cast_nonneg _)) this
  -- the normalized moments are at most `B` for every `t ≤ k`
  have hBt : ∀ t ≤ k, mu g S k t / (n.choose t : ℝ) ≤ B := by
    intro t ht
    by_cases hts : t ≤ S.card
    · exact hB t hts
    · have : S.powersetCard t = ∅ := powersetCard_eq_empty.2 (by omega)
      rw [show mu g S k t = 0 by unfold MLS.mu; rw [this, sum_empty], zero_div]
      exact hB0
  -- the event as a union over slots
  let A : Slot n k ψ Γ κ → Finset (Finset U) := fun j =>
    S.powerset.filter (fun X => g X (k - j.1.1) ≤ ((j.1.2 : ℕ) : ℝ))
  let E : Slot n k ψ Γ κ → Set (Slot n k ψ Γ κ → Finset U) := fun j =>
    {o | o j ∈ ((A j : Finset (Finset U)) : Set (Finset U))}
  have hset : {o : Slot n k ψ Γ κ → Finset U |
      ∃ j, o j ⊆ S ∧ g (o j) (k - j.1.1) ≤ ((j.1.2 : ℕ) : ℝ)} = ⋃ j, E j := by
    ext o
    simp [E, A, mem_filter, mem_powerset]
  -- one slot
  have hEj : ∀ j : Slot n k ψ Γ κ, (μ (E j)).toReal ≤ (2:ℝ) ^ ((j.1.2 : ℕ) : ℝ) * B := by
    intro j
    set t : ℕ := (j.1.1 : ℕ) with ht
    set θ : ℕ := (j.1.2 : ℕ) with hθ
    have htk : t ≤ k := Nat.lt_succ_iff.1 j.1.1.isLt
    have htn : t ≤ n := htk.trans hk
    have hC : (0:ℝ) < n.choose t := Nat.cast_pos.2 (Nat.choose_pos htn)
    set T : Finset (Finset U) := powersetCard t (univ : Finset U) with hT
    set F := (S.powersetCard t).filter (fun X => g X (k - t) ≤ (θ : ℝ)) with hF
    have hTA : T ∩ A j ⊆ F := by
      intro X hX
      rw [mem_inter, mem_powersetCard] at hX
      simp only [A, mem_filter, mem_powerset] at hX
      rw [hF, mem_filter, mem_powersetCard]
      exact ⟨⟨hX.2.1, hX.1.2⟩, hX.2.2⟩
    have hFmu : (F.card : ℝ) * (2:ℝ) ^ (-(θ : ℝ)) ≤ mu g S k t := by
      unfold MLS.mu
      calc (F.card : ℝ) * (2:ℝ) ^ (-(θ : ℝ)) = ∑ X ∈ F, (2:ℝ) ^ (-(θ : ℝ)) := by
            rw [sum_const, nsmul_eq_mul]
        _ ≤ ∑ X ∈ F, (2:ℝ) ^ (-(g X (k - t))) := by
            apply sum_le_sum
            intro X hX
            rw [hF, mem_filter] at hX
            exact Real.rpow_le_rpow_of_exponent_le (by norm_num) (by linarith [hX.2])
        _ ≤ ∑ X ∈ S.powersetCard t, (2:ℝ) ^ (-(g X (k - t))) :=
            sum_le_sum_of_subset_of_nonneg (filter_subset _ _) (fun _ _ _ => by positivity)
    have h2θ : (2:ℝ) ^ (θ : ℝ) * (2:ℝ) ^ (-(θ : ℝ)) = 1 := by
      rw [← Real.rpow_add (by norm_num)]; simp
    have hFle : (F.card : ℝ) ≤ (2:ℝ) ^ (θ : ℝ) * mu g S k t := by
      calc (F.card : ℝ) = (2:ℝ) ^ (θ : ℝ) * ((F.card : ℝ) * (2:ℝ) ^ (-(θ : ℝ))) := by
            rw [mul_comm (F.card : ℝ), ← mul_assoc, h2θ, one_mul]
        _ ≤ (2:ℝ) ^ (θ : ℝ) * mu g S k t := by gcongr
    have hE : E j = Set.pi Set.univ (fun i => if i = j then ((A j : Finset (Finset U)) :
        Set (Finset U)) else Set.univ) := by
      ext o
      simp only [E, Set.mem_setOf_eq, Set.mem_pi, Set.mem_univ, true_implies]
      constructor
      · intro h i
        split_ifs with hi
        · subst hi; exact h
        · exact Set.mem_univ _
      · intro h
        simpa using h j
    rw [hE, hμ]
    unfold trialMeasure
    rw [MeasureTheory.Measure.pi_pi, ENNReal.toReal_prod, Finset.prod_eq_single j]
    · rw [if_pos rfl, ProbabilityTheory.uniformOn_apply_finset, ENNReal.toReal_div,
        ENNReal.toReal_natCast, ENNReal.toReal_natCast, card_powersetCard, card_univ]
      have hcard : ((T ∩ A j).card : ℝ) ≤ F.card := by exact_mod_cast card_le_card hTA
      calc ((T ∩ A j).card : ℝ) / (n.choose t : ℝ)
          ≤ (2:ℝ) ^ (θ : ℝ) * mu g S k t / (n.choose t : ℝ) := by
            gcongr
            exact hcard.trans hFle
        _ = (2:ℝ) ^ (θ : ℝ) * (mu g S k t / (n.choose t : ℝ)) := by ring
        _ ≤ (2:ℝ) ^ (θ : ℝ) * B := by gcongr; exact hBt t htk
    · intro i _ hij
      rw [if_neg hij]
      haveI := hfac i
      rw [MeasureTheory.measure_univ, ENNReal.toReal_one]
    · intro h; exact absurd (Finset.mem_univ j) h
  -- one pair `(t, θ)`
  have hpair : ∀ θ : ℕ, θ ≤ Θ → (trials n ψ Γ κ θ : ℝ) * (2:ℝ) ^ (θ : ℝ)
      ≤ 4 * Γ * (2:ℝ) ^ (ψ * n) * (κ * ((Θ : ℝ) + 1) + 1) := by
    intro θ hθ
    have hΓ0 : (0:ℝ) ≤ Γ := by linarith
    have harg : 0 ≤ 4 * κ * Γ * ((Θ : ℝ) + 1) * (2:ℝ) ^ (ψ * n - θ) := by positivity
    have hc := Nat.ceil_lt_add_one harg
    have hsplit : (2:ℝ) ^ (ψ * n - θ) * (2:ℝ) ^ (θ : ℝ) = (2:ℝ) ^ (ψ * n) := by
      rw [← Real.rpow_add (by norm_num)]; ring_nf
    have hcap := cap_pow_le n ψ Γ hψ hΓ
    have hθΘ : (2:ℝ) ^ (θ : ℝ) ≤ (2:ℝ) ^ Θ := by
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_le (by norm_num) (by exact_mod_cast hθ)
    have hp0 : (0:ℝ) ≤ (2:ℝ) ^ (θ : ℝ) := by positivity
    have ht : (trials n ψ Γ κ θ : ℝ) ≤ 4 * κ * Γ * ((Θ : ℝ) + 1) * (2:ℝ) ^ (ψ * n - θ) + 1 := by
      unfold trials; exact hc.le
    calc (trials n ψ Γ κ θ : ℝ) * (2:ℝ) ^ (θ : ℝ)
        ≤ (4 * κ * Γ * ((Θ : ℝ) + 1) * (2:ℝ) ^ (ψ * n - θ) + 1) * (2:ℝ) ^ (θ : ℝ) :=
          mul_le_mul_of_nonneg_right ht hp0
      _ = 4 * κ * Γ * ((Θ : ℝ) + 1) * (2:ℝ) ^ (ψ * n) + (2:ℝ) ^ (θ : ℝ) := by
          rw [add_mul, mul_assoc (4 * κ * Γ * ((Θ : ℝ) + 1)), hsplit, one_mul]
      _ ≤ 4 * κ * Γ * ((Θ : ℝ) + 1) * (2:ℝ) ^ (ψ * n) + 4 * Γ * (2:ℝ) ^ (ψ * n) := by
          linarith
      _ = 4 * Γ * (2:ℝ) ^ (ψ * n) * (κ * ((Θ : ℝ) + 1) + 1) := by ring
  -- assemble
  rw [hset]
  have hfin : ∀ j ∈ (univ : Finset (Slot n k ψ Γ κ)), μ (E j) ≠ ⊤ :=
    fun j _ => MeasureTheory.measure_ne_top μ _
  have hΓ0 : (0:ℝ) ≤ Γ := by linarith
  calc (μ (⋃ j, E j)).toReal ≤ (∑ j, μ (E j)).toReal :=
        ENNReal.toReal_mono (ENNReal.sum_ne_top.2 hfin)
          (MeasureTheory.measure_iUnion_fintype_le μ E)
    _ = ∑ j, (μ (E j)).toReal := ENNReal.toReal_sum hfin
    _ ≤ ∑ j : Slot n k ψ Γ κ, (2:ℝ) ^ ((j.1.2 : ℕ) : ℝ) * B := sum_le_sum fun j _ => hEj j
    _ = ∑ p : Fin (k + 1) × Fin (Θ + 1),
          (trials n ψ Γ κ p.2 : ℝ) * (2:ℝ) ^ ((p.2 : ℕ) : ℝ) * B := by
        rw [Fintype.sum_sigma]
        refine sum_congr rfl fun p _ => ?_
        simp only [sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul]
        ring
    _ ≤ ∑ _p : Fin (k + 1) × Fin (Θ + 1),
          4 * Γ * (2:ℝ) ^ (ψ * n) * (κ * ((Θ : ℝ) + 1) + 1) * B :=
        sum_le_sum fun p _ =>
          mul_le_mul_of_nonneg_right (hpair p.2 (Nat.lt_succ_iff.1 p.2.isLt)) hB0
    _ = ((k : ℝ) + 1) * ((Θ : ℝ) + 1) *
          (4 * Γ * (2:ℝ) ^ (ψ * n) * (κ * ((Θ : ℝ) + 1) + 1) * B) := by
        rw [sum_const, card_univ, Fintype.card_prod, Fintype.card_fin, Fintype.card_fin,
          nsmul_eq_mul]
        push_cast; ring
    _ ≤ Pnec n k ψ Γ κ * (2:ℝ) ^ (ψ * n) * B := by
        unfold Pnec
        rw [← hΘ]
        have h1 : 0 ≤ ((k : ℝ) + 1) * ((Θ : ℝ) + 1) * (Γ * (2:ℝ) ^ (ψ * n) *
            (κ * ((Θ : ℝ) + 1) + 1) * B) := by positivity
        nlinarith

end MaxLeafFormal.MLSNec