theorem FABL.exercise9_1 {b B : ℝ} (hb : 1 < b)
  (hbB : b < B) :
  ∃ p X,
    FABL.IsReasonable p b X ∧
      ¬FABL.IsReasonable p B fun x =>
          1 + X x

theorem FABL.reasonable_three_add_const.{u_1}
  {Ω : Type u_1} [Fintype Ω] (p : PMF Ω)
  (X : Ω → ℝ) (c : ℝ)
  (hmean : FABL.pmfExpectation p X = 0)
  (hthird :
    (FABL.pmfExpectation p fun x =>
        X x ^ 3) =
      0)
  (hX : FABL.IsReasonable p 3 X) :
  FABL.IsReasonable p 3 fun x => c + X x

theorem FABL.linearForm_threeReasonable {n : ℕ}
  (a : Fin n → ℝ) :
  FABL.IsReasonable
    (FABL.uniformPMF (FABL.SignCube n)) 3
    (FABL.linearForm a)

theorem FABL.exercise9_2_uniformBits {n : ℕ}
  (c : ℝ) (a : Fin n → ℝ) :
  FABL.IsReasonable
    (FABL.uniformPMF (FABL.SignCube n)) 3
    fun x => c + FABL.linearForm a x

theorem FABL.exercise9_2_independent_threeReasonable.{u_1}
  {n : ℕ} {Ω : Fin n → Type u_1}
  [(i : Fin n) → Fintype (Ω i)]
  (p : (i : Fin n) → PMF (Ω i))
  (X : (i : Fin n) → Ω i → ℝ)
  (a : Finset (Fin n) → ℝ)
  (hmean :
    ∀ (i : Fin n),
      FABL.pmfExpectation (p i) (X i) = 0)
  (hthird :
    ∀ (i : Fin n),
      (FABL.pmfExpectation (p i) fun z =>
          X i z ^ 3) =
        0)
  (hreasonable :
    ∀ (i : Fin n),
      FABL.IsReasonable (p i) 3 (X i))
  (hdegree :
    FABL.MultilinearDegreeAtMost a 1) :
  FABL.IsReasonable
    (FABL.independentProductPMF p) 3
    (FABL.productMultilinearRandomVariable
      a X)

theorem FABL.DisjointBlockChoices.blocks_length.{u_1}
  {α : Type u_1} [DecidableEq α]
  {remaining : Finset α} {d t : ℕ}
  (choice :
    FABL.DisjointBlockChoices remaining d
      t) :
  (FABL.DisjointBlockChoices.blocks t
        choice).length =
    t

theorem FABL.DisjointBlockChoices.blocks_card.{u_1}
  {α : Type u_1} [DecidableEq α]
  {remaining : Finset α} {d t : ℕ}
  (choice :
    FABL.DisjointBlockChoices remaining d
      t)
  {block : Finset α}
  (hblock :
    block ∈
      FABL.DisjointBlockChoices.blocks t
        choice) :
  block.card = d

theorem FABL.DisjointBlockChoices.blocks_subset.{u_1}
  {α : Type u_1} [DecidableEq α]
  {remaining : Finset α} {d t : ℕ}
  (choice :
    FABL.DisjointBlockChoices remaining d
      t)
  {block : Finset α}
  (hblock :
    block ∈
      FABL.DisjointBlockChoices.blocks t
        choice) :
  block ⊆ remaining

theorem FABL.DisjointBlockChoices.blocks_pairwiseDisjoint.{u_1}
  {α : Type u_1} [DecidableEq α]
  {remaining : Finset α} {d t : ℕ}
  (choice :
    FABL.DisjointBlockChoices remaining d
      t) :
  List.Pairwise Disjoint
    (FABL.DisjointBlockChoices.blocks t
      choice)

theorem FABL.DisjointBlockChoices.ext_of_blocks_eq.{u}
  {α : Type u} [DecidableEq α]
  {remaining : Finset α} {d t : ℕ}
  (first second :
    FABL.DisjointBlockChoices remaining d
      t)
  (hblocks :
    FABL.DisjointBlockChoices.blocks t
        first =
      FABL.DisjointBlockChoices.blocks t
        second) :
  first = second

theorem FABL.SixDisjointBlockChoice.block_card
  {n d : ℕ}
  (choice :
    FABL.SixDisjointBlockChoice n d)
  (i : Fin 6) : (choice.block i).card = d

theorem FABL.SixDisjointBlockChoice.block_pairwiseDisjoint
  {n d : ℕ}
  (choice :
    FABL.SixDisjointBlockChoice n d) :
  Pairwise fun i j =>
    Disjoint (choice.block i)
      (choice.block j)

theorem FABL.natCard_powersetCardSubtype.{u}
  {α : Type u} (remaining : Finset α)
  (d : ℕ) :
  Nat.card
      ↥(Finset.powersetCard d remaining) =
    remaining.card.choose d

theorem FABL.natCard_disjointBlockChoices.{u}
  {α : Type u} [DecidableEq α]
  (remaining : Finset α) (d t : ℕ) :
  Nat.card
      (FABL.DisjointBlockChoices remaining
        d t) =
    ∏ j ∈ Finset.range t,
      (remaining.card - j * d).choose d

theorem FABL.natCard_sixDisjointBlockChoice
  (n d : ℕ) :
  Nat.card
      (FABL.SixDisjointBlockChoice n d) =
    ∏ j ∈ Finset.range 6,
      (n - j * d).choose d

theorem FABL.prod_choose_sub_mul_factorials
  (n d t : ℕ) (hdt : t * d ≤ n) :
  (∏ j ∈ Finset.range t,
          (n - j * d).choose d) *
        d.factorial ^ t *
      (n - t * d).factorial =
    n.factorial

theorem FABL.natCard_sixDisjointBlockChoice_eq_multinomial
  (n d : ℕ) (hnd : 6 * d ≤ n) :
  Nat.card
      (FABL.SixDisjointBlockChoice n d) =
    FABL.sixBlockMultinomial n d

theorem FABL.card_k4IncidentEdges (v : Fin 4) :
  (FABL.k4IncidentEdges v).card = 3

theorem FABL.SixDisjointBlockChoice.incidentSupport_card
  {n d : ℕ}
  (choice :
    FABL.SixDisjointBlockChoice n d)
  (v : Fin 4) :
  (choice.incidentSupport v).card = 3 * d

theorem FABL.SixDisjointBlockChoice.eq_of_mem_blocks
  {n d : ℕ}
  (choice :
    FABL.SixDisjointBlockChoice n d)
  {x : Fin n} {i j : Fin 6}
  (hi : x ∈ choice.block i)
  (hj : x ∈ choice.block j) : i = j

theorem FABL.tupleSymmDiff_finFour.{u_1}
  {α : Type u_1} [DecidableEq α]
  (sets : Fin 4 → Finset α) :
  FABL.tupleSymmDiff sets =
    symmDiff (sets 0)
      (symmDiff (sets 1)
        (symmDiff (sets 2)
          (symmDiff (sets 3) ∅)))

theorem FABL.SixDisjointBlockChoice.tupleSymmDiff_incidentSupport
  {n d : ℕ}
  (choice :
    FABL.SixDisjointBlockChoice n d) :
  (FABL.tupleSymmDiff fun v =>
      choice.incidentSupport v) =
    ∅

theorem FABL.SixDisjointBlockChoice.block_eq_incidentSupport_inter
  {n d : ℕ}
  (choice :
    FABL.SixDisjointBlockChoice n d)
  (edge : Fin 6) :
  choice.block edge =
    choice.incidentSupport
        (FABL.k4EdgeEnds edge).1 ∩
      choice.incidentSupport
        (FABL.k4EdgeEnds edge).2

theorem FABL.fourierCoeff_levelKPolynomial {n : ℕ}
  (k : ℕ) (T : Finset (Fin n)) :
  FABL.fourierCoeff
      (FABL.levelKPolynomial k) T =
    if T.card = k then 1 else 0

theorem FABL.expect_levelKPolynomial_sq
  (n k : ℕ) :
  (Finset.univ.expect fun x =>
      FABL.levelKPolynomial k x ^ 2) =
    ↑(n.choose k)

theorem FABL.SixDisjointBlockChoice.toParityTuple_injective
  {n d : ℕ} :
  Function.Injective
    FABL.SixDisjointBlockChoice.toParityTuple

theorem FABL.expect_levelKPolynomial_pow_eq_natCard_parityTuple
  (n k q : ℕ) :
  (Finset.univ.expect fun x =>
      FABL.levelKPolynomial k x ^ q) =
    ↑(Nat.card
        (FABL.LevelKParityTuple n k q))

theorem FABL.natCard_le_fourthMoment_levelKPolynomial_of_injective.{u_1}
  {W : Type u_1} [Finite W] (n k : ℕ)
  (encode :
    W → FABL.LevelKParityTuple n k 4)
  (hencode : Function.Injective encode) :
  ↑(Nat.card W) ≤
    Finset.univ.expect fun x =>
      FABL.levelKPolynomial k x ^ 4

theorem FABL.sixBlockMultinomial_le_fourthMoment_levelKPolynomial
  (n d : ℕ) (hnd : 6 * d ≤ n) :
  ↑(FABL.sixBlockMultinomial n d) ≤
    Finset.univ.expect fun x =>
      FABL.levelKPolynomial (3 * d) x ^ 4

theorem FABL.exercise9_3_fourthMoment_lower_bound
  (n d : ℕ) (hnd : 6 * d ≤ n) :
  ↑(FABL.sixBlockMultinomial n d) /
        ↑(n.choose (3 * d)) ^ 2 *
      (Finset.univ.expect fun x =>
          FABL.levelKPolynomial (3 * d)
              x ^
            2) ^
        2 ≤
    Finset.univ.expect fun x =>
      FABL.levelKPolynomial (3 * d) x ^ 4

theorem FABL.exercise9_3_fourthMoment_lower_bound_of_dvd
  (n k : ℕ) (_hkpos : 0 < k) (hk : 3 ∣ k)
  (hn : 2 * k ≤ n) :
  ↑(FABL.sixBlockMultinomial n (k / 3)) /
        ↑(n.choose k) ^ 2 *
      (Finset.univ.expect fun x =>
          FABL.levelKPolynomial k x ^ 2) ^
        2 ≤
    Finset.univ.expect fun x =>
      FABL.levelKPolynomial k x ^ 4

theorem FABL.tendsto_fixedShiftFactorialRatio
  (d : ℕ) :
  Filter.Tendsto
    (fun m =>
      FABL.fixedShiftFactorialRatio m d)
    Filter.atTop (nhds 1)

theorem FABL.fixedShiftFactorialRatio_eq_factorial_ratio
  (m d : ℕ) :
  FABL.fixedShiftFactorialRatio m d =
    ↑(m + 3 * d).factorial ^ 2 /
      (↑(m + 6 * d).factorial *
        ↑m.factorial)

theorem FABL.sixBlockMultinomial_shift_mul_factorials
  (m d : ℕ) :
  FABL.sixBlockMultinomial (m + 6 * d) d *
        d.factorial ^ 6 *
      m.factorial =
    (m + 6 * d).factorial

theorem FABL.choose_three_mul_shift_mul_factorials
  (m d : ℕ) :
  (m + 6 * d).choose (3 * d) *
        (3 * d).factorial *
      (m + 3 * d).factorial =
    (m + 6 * d).factorial

theorem FABL.exercise9_3_ratio_shift_eq
  (m d : ℕ) :
  ↑(FABL.sixBlockMultinomial (m + 6 * d)
          d) /
      ↑((m + 6 * d).choose (3 * d)) ^ 2 =
    ↑(3 * d).factorial ^ 2 /
        ↑d.factorial ^ 6 *
      FABL.fixedShiftFactorialRatio m d

theorem FABL.tendsto_exercise9_3_multinomial_ratio
  (d : ℕ) :
  Filter.Tendsto
    (fun m =>
      ↑(FABL.sixBlockMultinomial
            (m + 6 * d) d) /
        ↑((m + 6 * d).choose (3 * d)) ^ 2)
    Filter.atTop
    (nhds
      (↑(3 * d).factorial ^ 2 /
        ↑d.factorial ^ 6))

theorem FABL.factorial_isEquivalent_factorialStirlingApprox :
  Asymptotics.IsEquivalent Filter.atTop
    (fun n => ↑n.factorial)
    FABL.factorialStirlingApprox

theorem FABL.factorialStirlingApprox_three_ratio_eq
  (d : ℕ) (hd : 0 < d) :
  FABL.factorialStirlingApprox (3 * d) ^
        2 /
      FABL.factorialStirlingApprox d ^ 6 =
    3 / (4 * Real.pi ^ 2) *
      (1 / ↑d ^ 2 * 3 ^ (6 * d))