@MaxLeafFormal.Antinorm3.PZ_add_Kcum : ∀ {Z : Finset (ℝ × ℝ × ℝ)} {P Δ : ℝ × ℝ × ℝ}, P ∈ MaxLeafFormal.Antinorm3.PZ Z → Δ ∈ MaxLeafFormal.Antinorm3.Kcum → P + Δ ∈ MaxLeafFormal.Antinorm3.PZ Z @MaxLeafFormal.Antinorm3.fin_nonneg_of_Kcum : ∀ {Δ : ℝ × ℝ × ℝ}, Δ ∈ MaxLeafFormal.Antinorm3.Kcum → 0 ≤ MaxLeafFormal.Antinorm3.fin Δ @MaxLeafFormal.Antinorm3.init_all : ∀ {Z : Finset (ℝ × ℝ × ℝ)}, (∀ z ∈ Z, 0 ≤ z) → ∀ {y e₁ e₂ : ℝ}, 0 < e₁ → 0 < e₂ → e₂ ≤ 1 → ∀ (j₀ : ℕ), (∀ j ≤ j₀, MaxLeafFormal.Antinorm3.init y j ∈ (e₁ * e₂ ^ j) • MaxLeafFormal.Antinorm3.PZ Z) → (y / 2, 0, 0) ∈ (e₁ * e₂ ^ (j₀ + 1)) • MaxLeafFormal.Antinorm3.PZ Z → ∀ (j : ℕ), MaxLeafFormal.Antinorm3.init y j ∈ (e₁ * e₂ ^ j) • MaxLeafFormal.Antinorm3.PZ Z @MaxLeafFormal.Antinorm3.merge_Kcum_left : ∀ {Δ Q : ℝ × ℝ × ℝ}, Δ ∈ MaxLeafFormal.Antinorm3.Kcum → 0 ≤ Q → MaxLeafFormal.Antinorm3.merge Δ Q ∈ MaxLeafFormal.Antinorm3.Kcum @MaxLeafFormal.Antinorm3.merge_Kcum_right : ∀ {Q Δ : ℝ × ℝ × ℝ}, 0 ≤ Q → Δ ∈ MaxLeafFormal.Antinorm3.Kcum → MaxLeafFormal.Antinorm3.merge Q Δ ∈ MaxLeafFormal.Antinorm3.Kcum @MaxLeafFormal.Antinorm3.merge_mem_smul_PZ : ∀ {Z : Finset (ℝ × ℝ × ℝ)}, (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.Antinorm3.merge z z' ∈ MaxLeafFormal.Antinorm3.PZ Z) → ∀ {η η' : ℝ}, 0 < η' → ∀ {P Q : ℝ × ℝ × ℝ}, P ∈ η • MaxLeafFormal.Antinorm3.PZ Z → Q ∈ η' • MaxLeafFormal.Antinorm3.PZ Z → 0 ≤ Q → MaxLeafFormal.Antinorm3.merge P Q ∈ (η * η') • MaxLeafFormal.Antinorm3.PZ Z @MaxLeafFormal.Antinorm3.smul_PZ_add_Kcum : ∀ {Z : Finset (ℝ × ℝ × ℝ)} {η : ℝ}, 0 < η → ∀ {P Δ : ℝ × ℝ × ℝ}, P ∈ η • MaxLeafFormal.Antinorm3.PZ Z → Δ ∈ MaxLeafFormal.Antinorm3.Kcum → P + Δ ∈ η • MaxLeafFormal.Antinorm3.PZ Z @MaxLeafFormal.Antinorm3.smul_PZ_mono : ∀ {Z : Finset (ℝ × ℝ × ℝ)}, (∀ z ∈ Z, 0 ≤ z) → ∀ {η η' : ℝ}, 0 < η' → η' ≤ η → ∀ {P : ℝ × ℝ × ℝ}, P ∈ η • MaxLeafFormal.Antinorm3.PZ Z → P ∈ η' • MaxLeafFormal.Antinorm3.PZ Z @MaxLeafFormal.Antinorm3.treeW_eq_fin : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {F : SimpleGraph V} [inst_2 : DecidableRel F.Adj] (hF : F.IsTree) (r : V) (ν : V → ℕ) (y : ℝ), MaxLeafFormal.treeW F ν y = MaxLeafFormal.Antinorm3.fin (MaxLeafFormal.Antinorm3.triple hF r ν y Finset.univ r) @MaxLeafFormal.Antinorm3.tree_bound_of_certificate : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (y e₁ e₂ : ℝ), 0 ≤ y → 0 < e₁ → 0 < e₂ → ∀ (Z : Finset (ℝ × ℝ × ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.Antinorm3.merge z z' ∈ MaxLeafFormal.Antinorm3.PZ Z) → (∀ (j : ℕ), MaxLeafFormal.Antinorm3.init y j ∈ (e₁ * e₂ ^ j) • MaxLeafFormal.Antinorm3.PZ Z) → ∀ (T : SimpleGraph V) [DecidableRel T.Adj], T.IsTree → ∀ (ν : V → ℕ), MaxLeafFormal.Antinorm3.cZ Z hZ * e₁ ^ Fintype.card V * e₂ ^ ∑ v, ν v ≤ MaxLeafFormal.treeW T ν y @MaxLeafFormal.Antinorm3.tree_bound_of_checks : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {Z : List (ℚ × ℚ × ℚ)} {pairs inits : List (List (ℕ × ℚ))} {tail : List (ℕ × ℚ)} {y e₁ e₂ c : ℚ} {m₀ : ℕ}, 0 ≤ y → 0 < e₁ → 0 < e₂ → e₂ ≤ 1 → MaxLeafFormal.Antinorm3.checkZ Z c = true → MaxLeafFormal.Antinorm3.checkPairs Z pairs = true → MaxLeafFormal.Antinorm3.checkInits Z y e₁ e₂ m₀ inits tail = true → ∀ (T : SimpleGraph V) [DecidableRel T.Adj], T.IsTree → ∀ (ν : V → ℕ), ↑c * ↑e₁ ^ Fintype.card V * ↑e₂ ^ ∑ v, ν v ≤ MaxLeafFormal.treeW T ν ↑y @MaxLeafFormal.Antinorm3.triple_D_mem : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {Z : Finset (ℝ × ℝ × ℝ)} {F : SimpleGraph V} [inst_2 : DecidableRel F.Adj] (hF : F.IsTree) (r : V) (ν : V → ℕ) {y e₁ e₂ : ℝ}, 0 ≤ y → 0 < e₁ → 0 < e₂ → (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.Antinorm3.merge z z' ∈ MaxLeafFormal.Antinorm3.PZ Z) → (∀ (j : ℕ), MaxLeafFormal.Antinorm3.init y j ∈ (e₁ * e₂ ^ j) • MaxLeafFormal.Antinorm3.PZ Z) → ∀ (v : V), MaxLeafFormal.Antinorm3.triple hF r ν y (MaxLeafFormal.Antinorm3.D hF r v) v ∈ (e₁ ^ (MaxLeafFormal.Antinorm3.D hF r v).card * e₂ ^ ∑ u ∈ MaxLeafFormal.Antinorm3.D hF r v, ν u) • MaxLeafFormal.Antinorm3.PZ Z @MaxLeafFormal.Antinorm3.triple_single : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {F : SimpleGraph V} [inst_2 : DecidableRel F.Adj] (hF : F.IsTree) (r : V) (ν : V → ℕ) (y : ℝ) (v : V), MaxLeafFormal.Antinorm3.triple hF r ν y {v} v = MaxLeafFormal.Antinorm3.init y (ν v) @MaxLeafFormal.Antinorm3.triple_split : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {F : SimpleGraph V} [inst_2 : DecidableRel F.Adj] (hF : F.IsTree) (r : V) (ν : V → ℕ) (y : ℝ) {A B : Finset V} {v w : V}, Disjoint A B → v ∈ A → w ∈ B → w ≠ r → MaxLeafFormal.CDS.par hF r w = v → (∀ a ∈ A, ∀ b ∈ B, F.Adj a b → a = v ∧ b = w) → (∀ u ∈ B, u ≠ w → u ≠ r ∧ MaxLeafFormal.CDS.par hF r u ∈ B) → (∀ u ∈ A, u ≠ r → MaxLeafFormal.CDS.par hF r u ∉ B) → MaxLeafFormal.Antinorm3.triple hF r ν y (A ∪ B) v = MaxLeafFormal.Antinorm3.merge (MaxLeafFormal.Antinorm3.triple hF r ν y A v) (MaxLeafFormal.Antinorm3.triple hF r ν y B w) @MaxLeafFormal.Budget.budgeted_sound : ∀ {U : Type u_1} (sol : Finset U → Prop) (k : ℕ) {ι : Type u_2} {Ω : ι → ℕ → Type u_3} (A : (i : ι) → (θ : ℕ) → Set (Ω i θ)), (∀ (i : ι) (θ : ℕ), ∀ x ∈ A i θ, ∃ S, sol S ∧ S.card ≤ k) → ∀ {Θ : ℕ} {m : ι → ℕ → ℕ} (o : MaxLeafFormal.Budget.BOutcome Ω Θ m), MaxLeafFormal.Budget.BAccepts A o → ∃ S, sol S ∧ S.card ≤ k @MaxLeafFormal.Budget.budgeted_success : ∀ {ι : Type u_1} [inst : Fintype ι] {Ω : ι → ℕ → Type u_2} [inst_1 : (i : ι) → (θ : ℕ) → MeasurableSpace (Ω i θ)] (P : (i : ι) → (θ : ℕ) → MeasureTheory.Measure (Ω i θ)) [∀ (i : ι) (θ : ℕ), MeasureTheory.IsProbabilityMeasure (P i θ)] (A : (i : ι) → (θ : ℕ) → Set (Ω i θ)), (∀ (i : ι) (θ : ℕ), MeasurableSet (A i θ)) → ∀ {Ξ : ι → Type u_3} [inst_3 : (i : ι) → MeasurableSpace (Ξ i)] (Q : (i : ι) → MeasureTheory.Measure (Ξ i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (Q i)] (ξ : (i : ι) → Ξ i → ENNReal), (∀ (i : ι), Measurable (ξ i)) → (∀ (i : ι) (θ : ℕ), (Q i).real (MaxLeafFormal.Budget.leEvent (ξ i) ↑θ) ≤ (P i θ).real (A i θ)) → ∀ (n : ℕ) (ω Γ κ : ℝ), 0 ≤ ω → 1 ≤ Γ → 0 < κ → ∀ (Θ : ℕ), ω * ↑n + Real.logb 2 Γ + 1 ≤ ↑Θ → ∀ (m : ι → ℕ → ℕ), (∀ (i : ι), ∀ θ ≤ Θ, MaxLeafFormal.Budget.Mcount n ω Γ κ Θ θ ≤ ↑(m i θ)) → (∃ i, 2 ^ (-(ω * ↑n)) / Γ ≤ ∫ (x : Ξ i), MaxLeafFormal.Budget.twoPowNeg (ξ i x) ∂Q i) → 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.budgetMeasure P Θ m).real {o | MaxLeafFormal.Budget.BAccepts A o} @MaxLeafFormal.Budget.budgeted_success_of_admissible : ∀ {ι : Type u_1} [inst : Fintype ι] {Ω : ι → ℕ → Type u_2} [inst_1 : (i : ι) → (θ : ℕ) → MeasurableSpace (Ω i θ)] (P : (i : ι) → (θ : ℕ) → MeasureTheory.Measure (Ω i θ)) [∀ (i : ι) (θ : ℕ), MeasureTheory.IsProbabilityMeasure (P i θ)] (A : (i : ι) → (θ : ℕ) → Set (Ω i θ)), (∀ (i : ι) (θ : ℕ), MeasurableSet (A i θ)) → ∀ {Ξ : ι → Type u_3} [inst_3 : (i : ι) → MeasurableSpace (Ξ i)] (Q : (i : ι) → MeasureTheory.Measure (Ξ i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (Q i)] (ξ : (i : ι) → Ξ i → ENNReal), (∀ (i : ι), Measurable (ξ i)) → (∀ (i : ι) (θ : ℕ), (Q i).real (MaxLeafFormal.Budget.leEvent (ξ i) ↑θ) ≤ (P i θ).real (A i θ)) → ∀ (n : ℕ) (ω Γ κ : ℝ), 0 ≤ ω → 1 ≤ Γ → 0 < κ → ∀ (Θ : ℕ) (m : ι → ℕ → ℕ), MaxLeafFormal.Budget.AdmissibleParams n ω Γ κ Θ m → (∃ i, 2 ^ (-(ω * ↑n)) / Γ ≤ ∫ (x : Ξ i), MaxLeafFormal.Budget.twoPowNeg (ξ i x) ∂Q i) → 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.budgetMeasure P Θ m).real {o | MaxLeafFormal.Budget.BAccepts A o} @MaxLeafFormal.Budget.cds_budgeted : ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ {Ω : ℕ → ℕ → ℕ → Type u_2} [inst_3 : (s t θ : ℕ) → MeasurableSpace (Ω s t θ)] (P : (s t θ : ℕ) → MeasureTheory.Measure (Ω s t θ)), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → MeasureTheory.IsProbabilityMeasure (P s t θ)) → ∀ (A : (s t θ : ℕ) → Set (Ω s t θ)), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → MeasurableSet (A s t θ)) → (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → ∀ x ∈ A s t θ, MaxLeafFormal.CDS.γc G ≤ s) → ∀ (ω Γ κ : ℝ), 0 ≤ ω → 1 ≤ Γ → 0 < κ → ∀ (Θ : ℕ → ℕ), (∀ (s : ℕ), 1 ≤ s → s ≤ Fintype.card V → ω * ↑(Fintype.card V) + Real.logb 2 Γ + 1 ≤ ↑(Θ s)) → ∀ (m : ℕ → ℕ → ℕ → ℕ), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s → MaxLeafFormal.Budget.Mcount (Fintype.card V) ω Γ κ (Θ s) θ ≤ ↑(m s t θ)) → ∀ {Ξ : ℕ → Type u_3} [inst_4 : (t : ℕ) → MeasurableSpace (Ξ t)] (Q : (t : ℕ) → MeasureTheory.Measure (Ξ t)), (∀ t ≤ MaxLeafFormal.CDS.γc G, MeasureTheory.IsProbabilityMeasure (Q t)) → ∀ (ξ : (t : ℕ) → Ξ t → ENNReal), (∀ t ≤ MaxLeafFormal.CDS.γc G, Measurable (ξ t)) → (∀ (t θ : ℕ), t ≤ MaxLeafFormal.CDS.γc G → (Q t).real (MaxLeafFormal.Budget.leEvent (ξ t) ↑θ) ≤ (P (MaxLeafFormal.CDS.γc G) t θ).real (A (MaxLeafFormal.CDS.γc G) t θ)) → (∃ t ≤ MaxLeafFormal.CDS.γc G, 2 ^ (-(ω * ↑(Fintype.card V))) / Γ ≤ ∫ (x : Ξ t), MaxLeafFormal.Budget.twoPowNeg (ξ t x) ∂Q t) → (∀ (o : MaxLeafFormal.Budget.CdsOutcome (Fintype.card V) Ω Θ m), MaxLeafFormal.CDS.γc G ≤ MaxLeafFormal.Budget.cdsOutput (Fintype.card V) A o) ∧ 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.cdsMeasure (Fintype.card V) P Θ m).real {o | MaxLeafFormal.Budget.cdsOutput (Fintype.card V) A o = MaxLeafFormal.CDS.γc G} @MaxLeafFormal.Budget.cds_budgeted_maxLeaf : ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ {Ω : ℕ → ℕ → ℕ → Type u_2} [inst_3 : (s t θ : ℕ) → MeasurableSpace (Ω s t θ)] (P : (s t θ : ℕ) → MeasureTheory.Measure (Ω s t θ)), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → MeasureTheory.IsProbabilityMeasure (P s t θ)) → ∀ (A : (s t θ : ℕ) → Set (Ω s t θ)), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → MeasurableSet (A s t θ)) → (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → ∀ x ∈ A s t θ, MaxLeafFormal.CDS.γc G ≤ s) → ∀ (ω Γ κ : ℝ), 0 ≤ ω → 1 ≤ Γ → 0 < κ → ∀ (Θ : ℕ → ℕ), (∀ (s : ℕ), 1 ≤ s → s ≤ Fintype.card V → ω * ↑(Fintype.card V) + Real.logb 2 Γ + 1 ≤ ↑(Θ s)) → ∀ (m : ℕ → ℕ → ℕ → ℕ), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s → MaxLeafFormal.Budget.Mcount (Fintype.card V) ω Γ κ (Θ s) θ ≤ ↑(m s t θ)) → ∀ {Ξ : ℕ → Type u_3} [inst_4 : (t : ℕ) → MeasurableSpace (Ξ t)] (Q : (t : ℕ) → MeasureTheory.Measure (Ξ t)), (∀ t ≤ MaxLeafFormal.CDS.γc G, MeasureTheory.IsProbabilityMeasure (Q t)) → ∀ (ξ : (t : ℕ) → Ξ t → ENNReal), (∀ t ≤ MaxLeafFormal.CDS.γc G, Measurable (ξ t)) → (∀ (t θ : ℕ), t ≤ MaxLeafFormal.CDS.γc G → (Q t).real (MaxLeafFormal.Budget.leEvent (ξ t) ↑θ) ≤ (P (MaxLeafFormal.CDS.γc G) t θ).real (A (MaxLeafFormal.CDS.γc G) t θ)) → (∃ t ≤ MaxLeafFormal.CDS.γc G, 2 ^ (-(ω * ↑(Fintype.card V))) / Γ ≤ ∫ (x : Ξ t), MaxLeafFormal.Budget.twoPowNeg (ξ t x) ∂Q t) → 3 ≤ Fintype.card V → 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.cdsMeasure (Fintype.card V) P Θ m).real {o | IsGreatest {ℓ | ∃ F ≤ G, F.IsTree ∧ MaxLeafFormal.CDS.numLeaves F = ℓ} (Fintype.card V - MaxLeafFormal.Budget.cdsOutput (Fintype.card V) A o)} @MaxLeafFormal.Budget.first_accepted : ∀ {U : Type u_1} [inst : Fintype U] (sol : Finset U → Prop), (∃ S, sol S) → ¬sol ∅ → ∀ {Ω : Type u_2} [inst_1 : MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (acc : ℕ → Ω → Prop), (∀ (s : ℕ) (o : Ω), 1 ≤ s → s ≤ Fintype.card U → acc s o → ∃ S, sol S ∧ S.card ≤ s) → have opt := sInf {s | ∃ S, sol S ∧ S.card = s}; (∀ (o : Ω), opt ≤ MaxLeafFormal.Budget.firstAccepted (Fintype.card U) fun s => acc s o) ∧ P.real {o | acc opt o} ≤ P.real {o | (MaxLeafFormal.Budget.firstAccepted (Fintype.card U) fun s => acc s o) = opt} @MaxLeafFormal.Budget.integral_twoPowNeg_pos : ∀ {Ξ : Type u_1} [inst : MeasurableSpace Ξ] (Q : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure Q] (ξ : Ξ → ENNReal), Measurable ξ → 0 < Q {x | ξ x < ⊤} → 0 < ∫ (x : Ξ), MaxLeafFormal.Budget.twoPowNeg (ξ x) ∂Q @MaxLeafFormal.Budget.threshold_prob : ∀ {Ξ : Type u_1} [inst : MeasurableSpace Ξ] (Q : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure Q] (ξ : Ξ → ENNReal), Measurable ξ → 0 < Q {x | ξ x < ⊤} → ∀ (Θ : ℕ), 2 ^ (-↑Θ) ≤ (∫ (x : Ξ), MaxLeafFormal.Budget.twoPowNeg (ξ x) ∂Q) / 2 → ∃ θ ≤ Θ, (∫ (x : Ξ), MaxLeafFormal.Budget.twoPowNeg (ξ x) ∂Q) / (4 * (↑Θ + 1)) ≤ Q.real (MaxLeafFormal.Budget.leEvent ξ ↑θ) * 2 ^ (-↑θ) @MaxLeafFormal.Budget.threshold_prob_upper : ∀ {Ξ : Type u_1} [inst : MeasurableSpace Ξ] (Q : MeasureTheory.Measure Ξ) [MeasureTheory.IsProbabilityMeasure Q] (ξ : Ξ → ENNReal), Measurable ξ → 0 < Q {x | ξ x < ⊤} → ∀ (θ : ℤ), Q.real (MaxLeafFormal.Budget.leEvent ξ ↑θ) * 2 ^ (-↑θ) ≤ ∫ (x : Ξ), MaxLeafFormal.Budget.twoPowNeg (ξ x) ∂Q @MaxLeafFormal.CCGibbs.Zpart_iso : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {W : Type u_2} [inst_2 : Fintype W] [inst_3 : DecidableEq W] {F : SimpleGraph V} {G : SimpleGraph W} (e : F ≃g G) (ζ : ℝ), MaxLeafFormal.CCGibbs.Zpart F ζ = MaxLeafFormal.CCGibbs.Zpart G ζ @MaxLeafFormal.CCGibbs.cc_gibbs : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (F : SimpleGraph V), F.IsTree → ∀ (ζ : ℝ), 0 < ζ → min 1 ζ * MaxLeafFormal.CCRate.spr ζ ^ (Fintype.card V - 1) ≤ MaxLeafFormal.CCGibbs.Zpart F ζ @MaxLeafFormal.CCGibbs.cc_path : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (k : ℕ), 1 ≤ k → ∀ (F : SimpleGraph V) (e : F ≃g SimpleGraph.pathGraph k) (ζ : ℝ), 0 ≤ ζ → MaxLeafFormal.CCGibbs.Zpart F ζ ≤ (1 + ζ) * MaxLeafFormal.CCRate.spr ζ ^ (k - 1) ∧ (1 + ζ) * MaxLeafFormal.CCRate.spr ζ ^ (k - 1) ≤ 2 * MaxLeafFormal.CCRate.spr ζ ^ k @MaxLeafFormal.CCGibbs.cc_path_min : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (F : SimpleGraph V), F.IsTree → ∀ (ζ : ℝ), 0 < ζ → min 1 ζ / (1 + ζ) * MaxLeafFormal.CCGibbs.Zpart (SimpleGraph.pathGraph (Fintype.card V)) ζ ≤ MaxLeafFormal.CCGibbs.Zpart F ζ @MaxLeafFormal.CCGibbs.eIn_eq_induce : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (F : SimpleGraph V) (X : Finset V), MaxLeafFormal.CCGibbs.eIn F X = (SimpleGraph.induce (↑X) F).edgeFinset.card MaxLeafFormal.CCGibbs.spr_eigen : ∀ (ζ : ℝ), 0 ≤ ζ → (MaxLeafFormal.CCGibbs.Mz ζ).charpoly = Polynomial.X ^ 2 - Polynomial.C (1 + 2 * ζ) * Polynomial.X + Polynomial.C ζ ∧ (MaxLeafFormal.CCGibbs.Mz ζ).charpoly = (Polynomial.X - Polynomial.C (MaxLeafFormal.CCRate.spr ζ)) * (Polynomial.X - Polynomial.C (ζ / MaxLeafFormal.CCRate.spr ζ)) ∧ 0 ≤ ζ / MaxLeafFormal.CCRate.spr ζ ∧ ζ / MaxLeafFormal.CCRate.spr ζ ≤ MaxLeafFormal.CCRate.spr ζ ∧ ∀ (μ : ℂ), (Polynomial.aeval μ) (MaxLeafFormal.CCGibbs.Mz ζ).charpoly = 0 → ‖μ‖ ≤ MaxLeafFormal.CCRate.spr ζ MaxLeafFormal.CCGibbs.spr_facts : MaxLeafFormal.CCRate.spr 0 = 1 ∧ ContinuousOn MaxLeafFormal.CCRate.spr (Set.Ici 0) ∧ StrictMonoOn MaxLeafFormal.CCRate.spr (Set.Ici 0) ∧ (∀ (ζ : ℝ), 0 < ζ → 1 < MaxLeafFormal.CCRate.spr ζ) ∧ ∀ (ζ : ℝ), (1 + 2 * ζ) / 2 ≤ MaxLeafFormal.CCRate.spr ζ MaxLeafFormal.CCRate.cc_c3 : MaxLeafFormal.CCRate.spr (6 / 5) = 3 ∧ 6 / 5 / 3 < 3 ∧ 1 + 2 * (6 / 5) / 3 = 9 / 5 ∧ 3 ^ 64 < 5 ^ 45 ∧ Real.logb 2 (9 / 5) < MaxLeafFormal.MLS.H2 (26 / 45) MaxLeafFormal.CCRate.cc_cert : (∀ σ ∈ Set.Ioc 0 1, MaxLeafFormal.CCRate.R1 2 (71755 / 10 ^ 5) σ ∨ MaxLeafFormal.CCRate.R2 (71755 / 10 ^ 5) σ ∨ MaxLeafFormal.CCRate.R3 2 (71755 / 10 ^ 5) 16 σ) ∧ 71755 / 10 ^ 5 < Real.logb 2 (16444 / 10 ^ 4) MaxLeafFormal.CCRate.spr_root : ∀ (ζ : ℝ), MaxLeafFormal.CCRate.spr ζ ^ 2 - (1 + 2 * ζ) * MaxLeafFormal.CCRate.spr ζ + ζ = 0 @MaxLeafFormal.CCT.W_ge_Z : ∀ {U : Type u_1} [Fintype U] [inst : DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ), S.card = k → ∀ (c γ : ℝ), 1 ≤ c → ∀ (F : SimpleGraph ↥S), MaxLeafFormal.CCT.CCBoundOn g S k c γ F → ∀ (y : ℝ), 0 ≤ y → 2 ^ (-γ) * (c ^ k)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ≤ MaxLeafFormal.MLS.W g S k y @MaxLeafFormal.CCT.cc_T_a : ∀ {U : Type u_1} [inst : Fintype U] [inst_1 : DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ), S.card = k → ∀ (c γ : ℝ), 1 ≤ c → ∀ (F : SimpleGraph ↥S), F.IsTree → MaxLeafFormal.CCT.CCBoundOn g S k c γ F → ∀ (y : ℝ), 0 < y → 2 ^ (-γ) * (c ^ k)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ≤ MaxLeafFormal.MLS.W g S k y ∧ 2 ^ (-γ) * (min 1 (c * y / 2) / MaxLeafFormal.CCRate.spr (c * y / 2)) * (MaxLeafFormal.CCRate.spr (c * y / 2) / c) ^ k ≤ 2 ^ (-γ) * (c ^ k)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ∧ (1 + y) ^ Fintype.card U / MaxLeafFormal.MLS.W g S k y ≤ 2 ^ γ * (MaxLeafFormal.CCRate.spr (c * y / 2) / min 1 (c * y / 2)) * 2 ^ (↑(Fintype.card U) * MaxLeafFormal.CCRate.phi c (↑k / ↑(Fintype.card U)) y) @MaxLeafFormal.CCT.cc_T_a_of_gibbs : ∀ {U : Type u_1} [inst : Fintype U] [inst_1 : DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ), S.card = k → 1 ≤ k → ∀ (c γ : ℝ), 1 ≤ c → ∀ (F : SimpleGraph ↥S), MaxLeafFormal.CCT.CCBoundOn g S k c γ F → ∀ (y : ℝ), 0 < y → min 1 (c * y / 2) * MaxLeafFormal.CCRate.spr (c * y / 2) ^ (k - 1) ≤ MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) → 2 ^ (-γ) * (c ^ k)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ≤ MaxLeafFormal.MLS.W g S k y ∧ 2 ^ (-γ) * (min 1 (c * y / 2) / MaxLeafFormal.CCRate.spr (c * y / 2)) * (MaxLeafFormal.CCRate.spr (c * y / 2) / c) ^ k ≤ 2 ^ (-γ) * (c ^ k)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ∧ (1 + y) ^ Fintype.card U / MaxLeafFormal.MLS.W g S k y ≤ 2 ^ γ * (MaxLeafFormal.CCRate.spr (c * y / 2) / min 1 (c * y / 2)) * 2 ^ (↑(Fintype.card U) * MaxLeafFormal.CCRate.phi c (↑k / ↑(Fintype.card U)) y) @MaxLeafFormal.CCT.cc_T_a_of_hasCCBound : ∀ {U : Type u_1} [inst : Fintype U] [inst_1 : DecidableEq U] (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ) (c γ : ℝ), MaxLeafFormal.CCT.HasCCBound sol g c γ → ∀ (S : Finset U), sol S → 1 ≤ S.card → ∃ F, F.IsTree ∧ MaxLeafFormal.CCT.CCBoundOn g S S.card c γ F ∧ ∀ (y : ℝ), 0 < y → 2 ^ (-γ) * (c ^ S.card)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ≤ MaxLeafFormal.MLS.W g S S.card y ∧ 2 ^ (-γ) * (min 1 (c * y / 2) / MaxLeafFormal.CCRate.spr (c * y / 2)) * (MaxLeafFormal.CCRate.spr (c * y / 2) / c) ^ S.card ≤ 2 ^ (-γ) * (c ^ S.card)⁻¹ * MaxLeafFormal.CCGibbs.Zpart F (c * y / 2) ∧ (1 + y) ^ Fintype.card U / MaxLeafFormal.MLS.W g S S.card y ≤ 2 ^ γ * (MaxLeafFormal.CCRate.spr (c * y / 2) / min 1 (c * y / 2)) * 2 ^ (↑(Fintype.card U) * MaxLeafFormal.CCRate.phi c (↑S.card / ↑(Fintype.card U)) y) @MaxLeafFormal.CDS.maxLeaf_eq : ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → 3 ≤ Fintype.card V → IsGreatest {ℓ | ∃ F ≤ G, F.IsTree ∧ MaxLeafFormal.CDS.numLeaves F = ℓ} (Fintype.card V - MaxLeafFormal.CDS.γc G) @MaxLeafFormal.CDS.maxLeaf_small : ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), G.Connected → Fintype.card V ≤ 2 → G.IsTree ∧ (∀ F ≤ G, F.IsTree → F = G) ∧ (Fintype.card V = 1 → MaxLeafFormal.CDS.numLeaves G = 0) ∧ (Fintype.card V = 2 → MaxLeafFormal.CDS.numLeaves G = 2) @MaxLeafFormal.CDS.mean_terminals : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → 2 ≤ Fintype.card V → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ (t : ℕ), 1 ≤ t → t ≤ S.card → 1 + ↑t * (↑(Fintype.card V) - 2) / ↑S.card ≤ (∑ X ∈ Finset.powersetCard t S, (↑(MaxLeafFormal.CDS.closedNbhd G X).card - ↑(MaxLeafFormal.CDS.comp G X))) / ↑(S.card.choose t) ∧ (∑ X ∈ Finset.powersetCard t S, ↑(MaxLeafFormal.CDS.termCount G X)) / ↑(S.card.choose t) ≤ ↑(Fintype.card V) - 1 - ↑t * (↑(Fintype.card V) - 2) / ↑S.card MaxLeafFormal.CDS.moment_bound_of_tree_bound : ∀ (y c e₁ e₂ : ℝ), 0 ≤ y → (∀ (U : Type u_1) [inst : Fintype U] [inst_1 : DecidableEq U] (T : SimpleGraph U) [DecidableRel T.Adj], T.IsTree → ∀ (ν : U → ℕ), c * e₁ ^ Fintype.card U * e₂ ^ ∑ u, ν u ≤ MaxLeafFormal.treeW T ν y) → ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → c * e₁ ^ S.card * e₂ ^ (Fintype.card V - S.card) ≤ ∑ X ∈ S.powerset, y ^ X.card * (1 / 2) ^ MaxLeafFormal.CDS.termCount G X @MaxLeafFormal.CDS.pointwise : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], 2 ≤ Fintype.card V → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ (F : SimpleGraph V) [inst_3 : DecidableRel F.Adj], F ≤ G → F.IsTree → (∀ v ∉ S, F.degree v = 1) → ∑ u ∈ S, (↑(F.degree u) - 1) = ↑(Fintype.card V) - 2 ∧ ∀ X ⊆ S, X.Nonempty → 1 + ∑ x ∈ X, (↑(F.degree x) - 1) ≤ ↑(MaxLeafFormal.CDS.closedNbhd G X).card - ↑(MaxLeafFormal.CDS.comp G X) @MaxLeafFormal.CDS.rstheta_moment_bound_0 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → 6212 / 10000 * (747593601 / 960952792) ^ S.card * (512099210 / 652701491) ^ (Fintype.card V - S.card) ≤ ∑ X ∈ S.powerset, (69 / 200) ^ X.card * (1 / 2) ^ MaxLeafFormal.CDS.termCount G X @MaxLeafFormal.CDS.rstheta_moment_bound_1 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → 6293 / 10000 * (248231700 / 312721579) ^ S.card * (568097827 / 739289481) ^ (Fintype.card V - S.card) ≤ ∑ X ∈ S.powerset, (17 / 50) ^ X.card * (1 / 2) ^ MaxLeafFormal.CDS.termCount G X @MaxLeafFormal.CDS.spanningTree_of_CDS : ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∃ F ≤ G, F.IsTree ∧ (∀ v ∉ S, Nat.card ↑(F.neighborSet v) = 1) ∧ Fintype.card V - S.card ≤ MaxLeafFormal.CDS.numLeaves F @MaxLeafFormal.CDS.tree_inequality : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (F : SimpleGraph V) [inst_2 : DecidableRel F.Adj], F.IsTree → ∀ (X : Finset V), X.Nonempty → 1 + ∑ x ∈ X, (↑(F.degree x) - 1) ≤ ↑(MaxLeafFormal.CDS.closedNbhd F X).card - ↑(MaxLeafFormal.CDS.comp F X) @MaxLeafFormal.CDS.tree_reduction : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : { v // v ∉ S } → ↥S), (∀ (v : { v // v ∉ S }), G.Adj ↑v ↑(o v)) → have ν := fun u => {v | o v = u}.card; (∀ (X : Finset ↥S), MaxLeafFormal.CDS.termCount G (Finset.map (Function.Embedding.subtype fun x => x ∈ S) X) ≤ MaxLeafFormal.treePotential F ν X) ∧ ∀ (y : ℝ), 0 ≤ y → MaxLeafFormal.treeW F ν y ≤ ∑ X ∈ S.powerset, y ^ X.card * (1 / 2) ^ MaxLeafFormal.CDS.termCount G X @MaxLeafFormal.DSTCert.checkCert_sound : ∀ {y e₁ e₂ : ℚ} {Z : List (ℚ × ℚ)} {pairs : List (List (ℕ × ℚ))} {c2 : List (ℕ × ℚ)} {c3 : List (List (ℕ × ℚ))}, MaxLeafFormal.DSTCert.checkCert y e₁ e₂ Z pairs c2 c3 = true → MaxLeafFormal.DSTCert.CertHyp (↑y) (↑e₁) (↑e₂) (MaxLeafFormal.DSTCert.ZL Z) MaxLeafFormal.DSTCert.dst_certs_exact : (∀ (j : Fin 3), MaxLeafFormal.DSTCert.CertHyp (↑(MaxLeafFormal.DSTCert.y j)) (↑(MaxLeafFormal.DSTCert.e₁ j)) (↑(MaxLeafFormal.DSTCert.e₂ j)) (MaxLeafFormal.DSTCert.ZR j)) ∧ (MaxLeafFormal.DSTCert.ZR 0).card = 27 ∧ (MaxLeafFormal.DSTCert.ZR 1).card = 10 ∧ (MaxLeafFormal.DSTCert.ZR 2).card = 28 ∧ 40 / 100 ≤ MaxLeafFormal.DSTCert.cZ (MaxLeafFormal.DSTCert.ZR 0) ⋯ * ↑(MaxLeafFormal.DSTCert.e₂ 0) ∧ 41 / 100 ≤ MaxLeafFormal.DSTCert.cZ (MaxLeafFormal.DSTCert.ZR 1) ⋯ * ↑(MaxLeafFormal.DSTCert.e₂ 1) ∧ 11 / 1000 ≤ MaxLeafFormal.DSTCert.cZ (MaxLeafFormal.DSTCert.ZR 2) ⋯ * ↑(MaxLeafFormal.DSTCert.e₂ 2) ∧ (∀ (j : Fin 3), 0 ≤ MaxLeafFormal.DSTCert.lam j) ∧ ∑ j, MaxLeafFormal.DSTCert.lam j = 1 MaxLeafFormal.DSTCert.dst_rates : (∀ (i : Fin 3), ∑ j, ↑(MaxLeafFormal.DSTCert.lam j) * MaxLeafFormal.DSTCert.alpha j i < 4569670 / 10 ^ 7) ∧ (∃ i, 4569669 / 10 ^ 7 ≤ ∑ j, ↑(MaxLeafFormal.DSTCert.lam j) * MaxLeafFormal.DSTCert.alpha j i) ∧ 457 / 1000 < Real.logb 2 (13727 / 10000) ∧ 137268 / 10 ^ 5 ≤ 2 ^ (457 / 1000) ∧ 2 ^ (457 / 1000) < 137269 / 10 ^ 5 MaxLeafFormal.DSTCert.dst_rec : ∀ (y : ℝ) (t : MaxLeafFormal.Antinorm8.RTree MaxLeafFormal.DSTCert.Kind), MaxLeafFormal.DSTCert.rootKind t = MaxLeafFormal.DSTCert.Kind.term → MaxLeafFormal.DSTCert.WA y t = (MaxLeafFormal.DSTCert.psi y t).1 MaxLeafFormal.DSTCert.dst_tree_bound : ∀ (y e₁ e₂ : ℝ) (Z : Finset (ℝ × ℝ)) (hZ : Z.Nonempty), MaxLeafFormal.DSTCert.CertHyp y e₁ e₂ Z → ∀ (t : MaxLeafFormal.Antinorm8.RTree MaxLeafFormal.DSTCert.Kind), MaxLeafFormal.DSTCert.NoSteinerLeaf t → MaxLeafFormal.DSTCert.cZ Z hZ * e₁ ^ MaxLeafFormal.DSTCert.count MaxLeafFormal.DSTCert.Kind.steiner t * e₂ ^ MaxLeafFormal.DSTCert.count MaxLeafFormal.DSTCert.Kind.term t ≤ (MaxLeafFormal.DSTCert.psi y t).1 MaxLeafFormal.DSTCert.dst_tree_bound_WA : ∀ (y e₁ e₂ : ℝ) (Z : Finset (ℝ × ℝ)) (hZ : Z.Nonempty), MaxLeafFormal.DSTCert.CertHyp y e₁ e₂ Z → ∀ (t : MaxLeafFormal.Antinorm8.RTree MaxLeafFormal.DSTCert.Kind), MaxLeafFormal.DSTCert.rootKind t = MaxLeafFormal.DSTCert.Kind.term → MaxLeafFormal.DSTCert.NoSteinerLeaf t → MaxLeafFormal.DSTCert.cZ Z hZ * e₁ ^ MaxLeafFormal.DSTCert.count MaxLeafFormal.DSTCert.Kind.steiner t * e₂ ^ MaxLeafFormal.DSTCert.count MaxLeafFormal.DSTCert.Kind.term t ≤ MaxLeafFormal.DSTCert.WA y t @MaxLeafFormal.DSTGraph.fa_dst_W : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {G : Digraph V} {r : V} {K S : Finset V}, r ∉ K → S ⊆ MaxLeafFormal.DSTGraph.nonterm r K → ∀ (A : MaxLeafFormal.DSTGraph.OutArb G r (MaxLeafFormal.DSTGraph.Kbar r K S)) {y : ℝ}, 0 ≤ y → MaxLeafFormal.DSTGraph.WAg A y ≤ MaxLeafFormal.DSTGraph.WS G r K S y @MaxLeafFormal.DSTGraph.fa_dst_WS_minimum : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {G : Digraph V} {r : V} {K S : Finset V}, r ∉ K → S ⊆ MaxLeafFormal.DSTGraph.nonterm r K → MaxLeafFormal.DSTGraph.Steiner G r K S → (∀ T ⊆ MaxLeafFormal.DSTGraph.nonterm r K, MaxLeafFormal.DSTGraph.Steiner G r K T → S.card ≤ T.card) → ∀ (j : Fin 3), MaxLeafFormal.DSTCert.cZ (MaxLeafFormal.DSTCert.ZR j) ⋯ * ↑(MaxLeafFormal.DSTCert.e₂ j) * ↑(MaxLeafFormal.DSTCert.e₁ j) ^ S.card * ↑(MaxLeafFormal.DSTCert.e₂ j) ^ K.card ≤ MaxLeafFormal.DSTGraph.WS G r K S ↑(MaxLeafFormal.DSTCert.y j) @MaxLeafFormal.DSTGraph.fa_dst_point : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {G : Digraph V} {r : V} {K S : Finset V}, r ∉ K → S ⊆ MaxLeafFormal.DSTGraph.nonterm r K → ∀ (A : MaxLeafFormal.DSTGraph.OutArb G r (MaxLeafFormal.DSTGraph.Kbar r K S)) {X : Finset V}, X ⊆ S → MaxLeafFormal.DSTGraph.gDST G r K X ≤ MaxLeafFormal.DSTGraph.PsiG A X @MaxLeafFormal.DSTGraph.fa_dst_point_eq : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {G : Digraph V} {r : V} {K S : Finset V}, r ∉ K → S ⊆ MaxLeafFormal.DSTGraph.nonterm r K → ∀ (A : MaxLeafFormal.DSTGraph.OutArb G r (MaxLeafFormal.DSTGraph.Kbar r K S)) {X : Finset V}, X ⊆ S → (∀ a ∈ MaxLeafFormal.DSTGraph.Kbar r K X, ∀ b ∈ MaxLeafFormal.DSTGraph.Kbar r K X, G.Adj a b ↔ b ≠ r ∧ A.par b = a) → MaxLeafFormal.DSTGraph.gDST G r K X = MaxLeafFormal.DSTGraph.PsiG A X MaxLeafFormal.DetRate.det_cert : ∀ u ∈ Set.Icc (15 / 100) (85 / 100), ∃ y ∈ {(1 + √5) / 8, 1 / 2, 5 / 16, 1 / 4, 27 / 128, 29 / 160}, MaxLeafFormal.DetRate.chi y u ≤ Real.logb 2 (√5 - 1 / 2) MaxLeafFormal.Lobster.M_mulVec : ∀ (y : ℝ) (P : Fin 3 → ℝ), MaxLeafFormal.Lobster.toT ((MaxLeafFormal.Lobster.M y).mulVec P) = MaxLeafFormal.Antinorm3.merge (MaxLeafFormal.Lobster.toT (MaxLeafFormal.Lobster.u y)) (MaxLeafFormal.Lobster.toT P) MaxLeafFormal.Lobster.lobster_lower : ∀ (L : ℕ), 1 ≤ L → ∀ y ∈ Set.Icc 0 (3 / 4), MaxLeafFormal.Lobster.f ⬝ᵥ (MaxLeafFormal.Lobster.M y ^ (L - 1)).mulVec (MaxLeafFormal.Lobster.u y) ≤ (1 + y) ^ (7 * L) / (171927 / 100000) ^ (7 * L) MaxLeafFormal.Lobster.lobster_upper : ∃ C, 0 < C ∧ ∀ (L : ℕ), 1 ≤ L → (1 + 3453 / 10000) ^ (7 * L) ≤ C * (171928 / 100000) ^ (7 * L) * MaxLeafFormal.Lobster.f ⬝ᵥ (MaxLeafFormal.Lobster.M (3453 / 10000) ^ (L - 1)).mulVec (MaxLeafFormal.Lobster.u (3453 / 10000)) MaxLeafFormal.Lobster.u_eq : ∀ (y : ℝ), MaxLeafFormal.Lobster.toT (MaxLeafFormal.Lobster.u y) = MaxLeafFormal.Antinorm3.merge (MaxLeafFormal.Antinorm3.merge (MaxLeafFormal.Antinorm3.init y 0) (MaxLeafFormal.Antinorm3.init y 2)) (MaxLeafFormal.Antinorm3.init y 2) MaxLeafFormal.LobsterGraph.Lam : (L : ℕ) → SimpleGraph (Fin L × Fin 7) MaxLeafFormal.LobsterGraph.Sstar : (L : ℕ) → Finset (Fin L × Fin 7) MaxLeafFormal.LobsterGraph.lobW_eq_matrix : ∀ (L : ℕ), 1 ≤ L → ∀ (y : ℝ), MaxLeafFormal.MLS.W (MaxLeafFormal.RateAssembly.gT (MaxLeafFormal.LobsterGraph.Lam L)) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) y = MaxLeafFormal.Lobster.f ⬝ᵥ (MaxLeafFormal.Lobster.M y ^ (L - 1)).mulVec (MaxLeafFormal.Lobster.u y) MaxLeafFormal.LobsterGraph.lob_moments_lower : ∃ C, 0 < C ∧ ∀ (L : ℕ), 1 ≤ L → ∃ t ≤ 3 * L, ↑((7 * L).choose t) ≤ C * (171928 / 100000) ^ (7 * L) * MaxLeafFormal.MLS.mu (MaxLeafFormal.RateAssembly.gT (MaxLeafFormal.LobsterGraph.Lam L)) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) t MaxLeafFormal.LobsterGraph.lob_moments_upper : ∀ (L : ℕ), 1 ≤ L → ∀ t ≤ 7 * L, MaxLeafFormal.MLS.mu (MaxLeafFormal.RateAssembly.gT (MaxLeafFormal.LobsterGraph.Lam L)) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) t / ↑((7 * L).choose t) ≤ (↑(7 * L) + 1) / (171927 / 100000) ^ (7 * L) @MaxLeafFormal.LobsterGraph.mu_mul_pow_le_W : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (g : Finset V → ℕ → ℝ) (S : Finset V) (k t : ℕ) (y : ℝ), 0 ≤ y → MaxLeafFormal.MLS.mu g S k t * y ^ t ≤ MaxLeafFormal.MLS.W g S k y MaxLeafFormal.LobsterGraph.pow_le_choose_mul : ∀ (n t : ℕ), t < n → (1 + ↑t / (↑n - ↑t)) ^ n ≤ (↑n + 1) * ↑(n.choose t) * (↑t / (↑n - ↑t)) ^ t MaxLeafFormal.LobsterGraph.rst_caterpillar_c : (∀ (L : ℕ), 1 ≤ L → ∀ t ≤ 7 * L, MaxLeafFormal.MLS.mu (MaxLeafFormal.RateAssembly.gT (MaxLeafFormal.LobsterGraph.Lam L)) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) t / ↑((7 * L).choose t) ≤ (↑(7 * L) + 1) / (171927 / 100000) ^ (7 * L)) ∧ ∃ C, 0 < C ∧ ∀ (L : ℕ), 1 ≤ L → ∃ t ≤ 3 * L, ↑((7 * L).choose t) ≤ C * (171928 / 100000) ^ (7 * L) * MaxLeafFormal.MLS.mu (MaxLeafFormal.RateAssembly.gT (MaxLeafFormal.LobsterGraph.Lam L)) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) t MaxLeafFormal.LobsterGraph.rst_caterpillar_c_of_agree : (∀ (L : ℕ), 1 ≤ L → ∀ (G : SimpleGraph (Fin L × Fin 7)) [inst : DecidableRel G.Adj], (∀ u ∈ MaxLeafFormal.LobsterGraph.Sstar L, ∀ (v : Fin L × Fin 7), G.Adj u v ↔ (MaxLeafFormal.LobsterGraph.Lam L).Adj u v) → ∀ t ≤ 7 * L, MaxLeafFormal.MLS.mu (MaxLeafFormal.RateAssembly.gT G) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) t / ↑((7 * L).choose t) ≤ (↑(7 * L) + 1) / (171927 / 100000) ^ (7 * L)) ∧ ∃ C, 0 < C ∧ ∀ (L : ℕ), 1 ≤ L → ∀ (G : SimpleGraph (Fin L × Fin 7)) [inst : DecidableRel G.Adj], (∀ u ∈ MaxLeafFormal.LobsterGraph.Sstar L, ∀ (v : Fin L × Fin 7), G.Adj u v ↔ (MaxLeafFormal.LobsterGraph.Lam L).Adj u v) → ∃ t ≤ 3 * L, ↑((7 * L).choose t) ≤ C * (171928 / 100000) ^ (7 * L) * MaxLeafFormal.MLS.mu (MaxLeafFormal.RateAssembly.gT G) (MaxLeafFormal.LobsterGraph.Sstar L) (3 * L) t @MaxLeafFormal.LobsterGraph.tree_reduction_eq : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (S : Finset V) (F : SimpleGraph ↥S), F = SimpleGraph.induce (↑S) G → ∀ (o : { v // v ∉ S } → ↥S), (∀ (v : { v // v ∉ S }), G.Adj ↑v ↑(o v)) → (∀ (v : { v // v ∉ S }) (w : ↥S), G.Adj ↑v ↑w → w = o v) → have ν := fun u => {v | o v = u}.card; ∀ (X : Finset ↥S), MaxLeafFormal.CDS.termCount G (Finset.map (Function.Embedding.subtype fun x => x ∈ S) X) = MaxLeafFormal.treePotential F ν X @MaxLeafFormal.MLS.linear_savings_W : ∀ {U : Type u_1} [inst : Fintype U] [DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ), S.card = k → ∀ (σ β ρ C : ℝ), σ = ↑k / ↑(Fintype.card U) → σ ∈ Set.Ioo 0 1 → 0 ≤ β → 0 ≤ ρ → 0 ≤ C → (∀ t ≤ k, (∑ X ∈ Finset.powersetCard t S, g X (k - t)) / ↑(k.choose t) ≤ β * ↑(Fintype.card U) - ρ * ↑t + C) → have y := if σ ≤ 2 ^ (-ρ) then 0 else (σ * 2 ^ ρ - 1) / (2 ^ ρ * (1 - σ)); (1 + y) ^ Fintype.card U / MaxLeafFormal.MLS.W g S k y ≤ 2 ^ (C + ↑(Fintype.card U) * MaxLeafFormal.MLS.Fstar σ β ρ) MaxLeafFormal.MLS.mls_budget : ∀ (n k : ℕ) (ω Γ κ : ℝ), 0 ≤ ω → 1 ≤ Γ → 0 < κ → 2 ^ MaxLeafFormal.MLS.cap n ω Γ ≤ 4 * Γ * 2 ^ (ω * ↑n) ∧ ∑ t ∈ Finset.range (k + 1), ∑ θ ∈ Finset.range (MaxLeafFormal.MLS.cap n ω Γ + 1), ↑(MaxLeafFormal.MLS.trials n ω Γ κ θ) * 2 ^ (θ + 1) ≤ (↑k + 1) * (↑(MaxLeafFormal.MLS.cap n ω Γ) + 1) * (8 * κ * Γ * (↑(MaxLeafFormal.MLS.cap n ω Γ) + 1) * 2 ^ (ω * ↑n) + 2 ^ (MaxLeafFormal.MLS.cap n ω Γ + 1)) @MaxLeafFormal.MLS.mls_sound : ∀ {U : Type u_1} [inst : Fintype U] [inst_1 : DecidableEq U] (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ) (k : ℕ) (ω Γ κ : ℝ) (o : MaxLeafFormal.MLS.Slot (Fintype.card U) k ω Γ κ → Finset U), (∀ (j : MaxLeafFormal.MLS.Slot (Fintype.card U) k ω Γ κ), (o j).card = ↑j.fst.1) → MaxLeafFormal.MLS.Accepts sol g k ω Γ κ o → ∃ S, sol S ∧ S.card ≤ k @MaxLeafFormal.MLS.mls_success : ∀ {U : Type u_1} [inst : Fintype U] [inst_1 : DecidableEq U] (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ), (∀ (X : Finset U) (k' : ℕ), 0 ≤ g X k') → ∀ k ≤ Fintype.card U, ∀ (ω Γ κ : ℝ), 0 ≤ ω → 1 ≤ Γ → 0 < κ → ∀ (S : Finset U), sol S → S.card = k → MaxLeafFormal.MLS.Star g S k ω Γ → 1 - Real.exp (-κ) ≤ ((MaxLeafFormal.MLS.trialMeasure k ω Γ κ) {o | MaxLeafFormal.MLS.Accepts sol g k ω Γ κ o}).toReal @MaxLeafFormal.MLS.mls_success_of_mean : ∀ {U : Type u_1} [inst : Fintype U] [inst_1 : DecidableEq U] (sol : Finset U → Prop) (g : Finset U → ℕ → ℝ), (∀ (X : Finset U) (k' : ℕ), 0 ≤ g X k') → ∀ (k t : ℕ), t ≤ k → 1 ≤ Fintype.card U → ∀ (lam κ : ℝ), 0 ≤ lam → 0 < κ → ∀ (S : Finset U), sol S → S.card = k → (∑ X ∈ Finset.powersetCard t S, g X (k - t)) / ↑(k.choose t) ≤ lam → have ω := (Real.logb 2 (↑((Fintype.card U).choose t) / ↑(k.choose t)) + lam) / ↑(Fintype.card U); 1 - Real.exp (-κ) ≤ ((MaxLeafFormal.MLS.trialMeasure k ω 1 κ) {o | MaxLeafFormal.MLS.Accepts sol g k ω 1 κ o}).toReal @MaxLeafFormal.MLS.mu_ge_of_mean : ∀ {U : Type u_1} [Fintype U] [DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k t : ℕ), S.card = k → t ≤ k → ∀ (lam : ℝ), (∑ X ∈ Finset.powersetCard t S, g X (k - t)) / ↑(k.choose t) ≤ lam → ↑(k.choose t) * 2 ^ (-lam) ≤ MaxLeafFormal.MLS.mu g S k t MaxLeafFormal.MLS.one_sample_size : ∀ (σ β ρ : ℝ), σ ∈ Set.Ioo 0 1 → 0 ≤ β → 0 ≤ ρ → StrictConvexOn ℝ (Set.Icc 0 σ) (MaxLeafFormal.MLS.fσ σ β ρ) ∧ MaxLeafFormal.MLS.τstar σ ρ ∈ Set.Icc 0 σ ∧ (∀ τ ∈ Set.Icc 0 σ, MaxLeafFormal.MLS.fσ σ β ρ τ = MaxLeafFormal.MLS.Fstar σ β ρ ↔ τ = MaxLeafFormal.MLS.τstar σ ρ) ∧ (∀ τ ∈ Set.Icc 0 σ, MaxLeafFormal.MLS.Fstar σ β ρ ≤ MaxLeafFormal.MLS.fσ σ β ρ τ) ∧ (MaxLeafFormal.MLS.Fstar σ β ρ < β ↔ Real.logb 2 (1 / σ) < ρ) @MaxLeafFormal.MLS.star_of_W : ∀ {U : Type u_1} [inst : Fintype U] [DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ), S.card = k → ∀ (ω Γ y : ℝ), 0 < Γ → 0 ≤ y → (1 + y) ^ Fintype.card U * 2 ^ (-(ω * ↑(Fintype.card U))) / Γ ≤ MaxLeafFormal.MLS.W g S k y → MaxLeafFormal.MLS.Star g S k ω Γ MaxLeafFormal.MLSNec.Pnec : ℕ → ℕ → ℝ → ℝ → ℝ → ℝ @MaxLeafFormal.MLSNec.fw_gf_upper : ∀ {U : Type u_1} [inst : Fintype U] [DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k : ℕ), S.card = k → ∀ t ≤ k, ∃ y, 0 ≤ y ∧ MaxLeafFormal.MLS.mu g S k t * (1 + y) ^ Fintype.card U ≤ (↑(Fintype.card U) + 1) * ↑((Fintype.card U).choose t) * MaxLeafFormal.MLS.W g S k y @MaxLeafFormal.MLSNec.mls_necessary : ∀ {U : Type u_1} [inst : Fintype U] [DecidableEq U] (g : Finset U → ℕ → ℝ), ∀ k ≤ Fintype.card U, ∀ (ψ Γ κ : ℝ), 0 ≤ ψ → 1 ≤ Γ → 0 < κ → ∀ (S : Finset U), S.card ≤ k → ∀ (B : ℝ), (∀ t ≤ S.card, MaxLeafFormal.MLS.mu g S k t / ↑((Fintype.card U).choose t) ≤ B) → ((MaxLeafFormal.MLS.trialMeasure k ψ Γ κ) {o | ∃ j, o j ⊆ S ∧ g (o j) (k - ↑j.fst.1) ≤ ↑↑j.fst.2}).toReal ≤ MaxLeafFormal.MLSNec.Pnec (Fintype.card U) k ψ Γ κ * 2 ^ (ψ * ↑(Fintype.card U)) * B @MaxLeafFormal.MLSNec.mu_mul_pow_le_W : ∀ {U : Type u_1} [Fintype U] [DecidableEq U] (g : Finset U → ℕ → ℝ) (S : Finset U) (k t : ℕ) (y : ℝ), 0 ≤ y → MaxLeafFormal.MLS.mu g S k t * y ^ t ≤ MaxLeafFormal.MLS.W g S k y MaxLeafFormal.MLSNec.pow_le_choose_mul : ∀ (n t : ℕ), t < n → (1 + ↑t / (↑n - ↑t)) ^ n ≤ (↑n + 1) * ↑(n.choose t) * (↑t / (↑n - ↑t)) ^ t MaxLeafFormal.PDGraph.Sstar_subset : ∀ (L : ℕ) (S : Finset (Fin L × Fin 6)), MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L) S → MaxLeafFormal.PDGraph.Sstar L ⊆ S @MaxLeafFormal.PDGraph.card_eq_sum_pairs : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) (S : Finset V) (P : Finset (V × V)), MaxLeafFormal.PDGraph.IsPairing G S P → ∀ (anc : V → V), MaxLeafFormal.PDGraph.IsAnchor G S anc → Fintype.card V = ∑ q ∈ P, (2 + MaxLeafFormal.PDGraph.ancDeg S anc q.1 + MaxLeafFormal.PDGraph.ancDeg S anc q.2) @MaxLeafFormal.PDGraph.exists_anchor : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (S : Finset V), MaxLeafFormal.PDGraph.IsDominating G S → ∃ anc, MaxLeafFormal.PDGraph.IsAnchor G S anc MaxLeafFormal.PDGraph.fa_pd_tight : (0 < MaxLeafFormal.PDRate.ystar ∧ (∀ (y : ℝ), 0 < y → DifferentiableAt ℝ (MaxLeafFormal.PDRate.hpd 6) y) ∧ (∀ (y : ℝ), 0 < y → (deriv (MaxLeafFormal.PDRate.hpd 6) y = 0 ↔ y = MaxLeafFormal.PDRate.ystar)) ∧ 0 ≤ MaxLeafFormal.PDRate.ystar ∧ ∀ (y : ℝ), 0 ≤ y → MaxLeafFormal.PDRate.ωpr ≤ MaxLeafFormal.PDRate.hpd 6 y) ∧ (∀ (L : ℕ), MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L) (MaxLeafFormal.PDGraph.Sstar L) ∧ (MaxLeafFormal.PDGraph.Sstar L).card = 2 * L ∧ ∀ (S : Finset (Fin L × Fin 6)), MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L) S → S.card ≤ 2 * L → S = MaxLeafFormal.PDGraph.Sstar L) ∧ ∀ (ψ' Γ κ : ℝ), 0 ≤ ψ' → ψ' < MaxLeafFormal.PDRate.ωpr → 1 ≤ Γ → 0 < κ → Filter.Tendsto (fun L => ((MaxLeafFormal.MLS.trialMeasure (2 * L) ψ' Γ κ) {o | MaxLeafFormal.MLS.Accepts (MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L)) (MaxLeafFormal.PDGraph.pdG (MaxLeafFormal.PDGraph.dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal) Filter.atTop (nhds 0) @MaxLeafFormal.PDGraph.matching_of_pairing : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (S : Finset V) (P : Finset (V × V)), MaxLeafFormal.PDGraph.IsPairing G S P → ∃ M, M.verts = ↑S ∧ M.IsMatching ∧ ∀ (a b : V), M.Adj a b ↔ (a, b) ∈ P ∨ (b, a) ∈ P @MaxLeafFormal.PDGraph.pairing_of_matching : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (S : Finset V) (M : G.Subgraph), M.verts = ↑S → M.IsMatching → ∃ P, MaxLeafFormal.PDGraph.IsPairing G S P ∧ ∀ (a b : V), M.Adj a b ↔ (a, b) ∈ P ∨ (b, a) ∈ P @MaxLeafFormal.PDGraph.pd_point : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (S : Finset V) (P : Finset (V × V)), MaxLeafFormal.PDGraph.IsPairing G S P → ∀ (anc : V → V), MaxLeafFormal.PDGraph.IsAnchor G S anc → (∀ X ⊆ S, (MaxLeafFormal.PDGraph.und G X).card ≤ MaxLeafFormal.PDGraph.pdRhs S P anc X) ∧ ∀ (y : ℝ), 0 ≤ y → ∏ q ∈ P, MaxLeafFormal.PDGraph.Ωpair y (MaxLeafFormal.PDGraph.ancDeg S anc q.1) (MaxLeafFormal.PDGraph.ancDeg S anc q.2) ≤ MaxLeafFormal.PDGraph.pdW G S y @MaxLeafFormal.PDGraph.pd_point_factor : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) (S : Finset V) (P : Finset (V × V)), MaxLeafFormal.PDGraph.IsPairing G S P → ∀ (anc : V → V), MaxLeafFormal.PDGraph.IsAnchor G S anc → ∀ (y : ℝ), ∑ X ∈ S.powerset, y ^ X.card * 2 ^ (-↑(MaxLeafFormal.PDGraph.pdRhs S P anc X)) = ∏ q ∈ P, MaxLeafFormal.PDGraph.Ωpair y (MaxLeafFormal.PDGraph.ancDeg S anc q.1) (MaxLeafFormal.PDGraph.ancDeg S anc q.2) @MaxLeafFormal.PDGraph.pd_rate_W : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], (∀ (v : V), ∃ u, G.Adj v u) → ∀ (S : Finset V), MaxLeafFormal.PDGraph.IsPairedDom G S → (1 + MaxLeafFormal.PDRate.ystar) ^ Fintype.card V * 2 ^ (-(MaxLeafFormal.PDRate.ωpr * ↑(Fintype.card V))) ≤ MaxLeafFormal.PDGraph.pdW G S MaxLeafFormal.PDRate.ystar @MaxLeafFormal.PDGraph.pd_star : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (S : Finset V), MaxLeafFormal.PDGraph.IsPairedDom G S → MaxLeafFormal.MLS.Star (MaxLeafFormal.PDGraph.pdG G) S S.card (70502 / 10 ^ 5) 1 @MaxLeafFormal.PDGraph.pd_success : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (S : Finset V), MaxLeafFormal.PDGraph.IsPairedDom G S → ∀ (κ : ℝ), 0 < κ → 1 - Real.exp (-κ) ≤ ((MaxLeafFormal.MLS.trialMeasure S.card (70502 / 10 ^ 5) 1 κ) {o | MaxLeafFormal.MLS.Accepts (MaxLeafFormal.PDGraph.IsPairedDom G) (MaxLeafFormal.PDGraph.pdG G) S.card (70502 / 10 ^ 5) 1 κ o}).toReal MaxLeafFormal.PDGraph.pd_tight_W : ∀ (L : ℕ) (y : ℝ), MaxLeafFormal.PDGraph.pdW (MaxLeafFormal.PDGraph.dstarGraph L) (MaxLeafFormal.PDGraph.Sstar L) y = (y ^ 2 + y / 2 + 1 / 64) ^ L MaxLeafFormal.PDGraph.pd_tight_W_le : ∀ (L : ℕ) (y : ℝ), 0 ≤ y → MaxLeafFormal.PDGraph.pdW (MaxLeafFormal.PDGraph.dstarGraph L) (MaxLeafFormal.PDGraph.Sstar L) y ≤ (1 + y) ^ (6 * L) * 2 ^ (-(MaxLeafFormal.PDRate.ωpr * ↑(6 * L))) MaxLeafFormal.PDGraph.pd_tight_accepts : ∀ (L : ℕ) (ψ Γ κ : ℝ) (o : MaxLeafFormal.MLS.Slot (Fintype.card (Fin L × Fin 6)) (2 * L) ψ Γ κ → Finset (Fin L × Fin 6)), (∀ (j : MaxLeafFormal.MLS.Slot (Fintype.card (Fin L × Fin 6)) (2 * L) ψ Γ κ), (o j).card = ↑j.fst.1) → MaxLeafFormal.MLS.Accepts (MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L)) (MaxLeafFormal.PDGraph.pdG (MaxLeafFormal.PDGraph.dstarGraph L)) (2 * L) ψ Γ κ o → ∃ j, o j ⊆ MaxLeafFormal.PDGraph.Sstar L ∧ MaxLeafFormal.PDGraph.pdG (MaxLeafFormal.PDGraph.dstarGraph L) (o j) (2 * L - ↑j.fst.1) ≤ ↑↑j.fst.2 MaxLeafFormal.PDGraph.pd_tight_argmin : ∀ (y : ℝ), 0 ≤ y → y ≠ MaxLeafFormal.PDRate.ystar → MaxLeafFormal.PDRate.ωpr < MaxLeafFormal.PDRate.hpd 6 y MaxLeafFormal.PDGraph.pd_tight_crit : 0 < MaxLeafFormal.PDRate.ystar ∧ (∀ (y : ℝ), 0 < y → DifferentiableAt ℝ (MaxLeafFormal.PDRate.hpd 6) y) ∧ ∀ (y : ℝ), 0 < y → (deriv (MaxLeafFormal.PDRate.hpd 6) y = 0 ↔ y = MaxLeafFormal.PDRate.ystar) MaxLeafFormal.PDGraph.pd_tight_min : 0 ≤ MaxLeafFormal.PDRate.ystar ∧ ∀ (y : ℝ), 0 ≤ y → MaxLeafFormal.PDRate.ωpr ≤ MaxLeafFormal.PDRate.hpd 6 y MaxLeafFormal.PDGraph.pd_tight_moments : ∀ (L t : ℕ), t ≤ 2 * L → MaxLeafFormal.MLS.mu (MaxLeafFormal.PDGraph.pdG (MaxLeafFormal.PDGraph.dstarGraph L)) (MaxLeafFormal.PDGraph.Sstar L) (2 * L) t / ↑((6 * L).choose t) ≤ (↑(6 * L) + 1) * 2 ^ (-(MaxLeafFormal.PDRate.ωpr * ↑(6 * L))) MaxLeafFormal.PDGraph.pd_tight_prob : ∀ (ψ' Γ κ : ℝ), 0 ≤ ψ' → ψ' < MaxLeafFormal.PDRate.ωpr → 1 ≤ Γ → 0 < κ → Filter.Tendsto (fun L => ((MaxLeafFormal.MLS.trialMeasure (2 * L) ψ' Γ κ) {o | MaxLeafFormal.MLS.Accepts (MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L)) (MaxLeafFormal.PDGraph.pdG (MaxLeafFormal.PDGraph.dstarGraph L)) (2 * L) ψ' Γ κ o}).toReal) Filter.atTop (nhds 0) MaxLeafFormal.PDGraph.pd_tight_ratio : ∀ (L : ℕ) (y : ℝ), 0 ≤ y → (1 + y) ^ (6 * L) = 2 ^ (↑(6 * L) * MaxLeafFormal.PDRate.hpd 6 y) * MaxLeafFormal.PDGraph.pdW (MaxLeafFormal.PDGraph.dstarGraph L) (MaxLeafFormal.PDGraph.Sstar L) y MaxLeafFormal.PDGraph.pd_tight_unique : ∀ (L : ℕ), MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L) (MaxLeafFormal.PDGraph.Sstar L) ∧ (MaxLeafFormal.PDGraph.Sstar L).card = 2 * L ∧ ∀ (S : Finset (Fin L × Fin 6)), MaxLeafFormal.PDGraph.IsPairedDom (MaxLeafFormal.PDGraph.dstarGraph L) S → S.card ≤ 2 * L → S = MaxLeafFormal.PDGraph.Sstar L MaxLeafFormal.PDGraph.Ωpair_amgm : ∀ (y : ℝ), 0 ≤ y → ∀ (du dv : ℕ), y ^ 2 + 4 * 2 ^ (-↑(2 + du + dv) / 2) * y + 2 ^ (-↑(2 + du + dv)) ≤ MaxLeafFormal.PDGraph.Ωpair y du dv MaxLeafFormal.PDRate.pd_constants : 16301556 / 10 ^ 7 ≤ 2 ^ MaxLeafFormal.PDRate.ωpr ∧ 2 ^ MaxLeafFormal.PDRate.ωpr < 16301557 / 10 ^ 7 ∧ MaxLeafFormal.PDRate.ωpr < 70502 / 10 ^ 5 ∧ 2 ^ (70502 / 10 ^ 5) < 16302 / 10 ^ 4 MaxLeafFormal.PDRate.pd_rate : (∀ (m : ℕ), 2 ≤ m → MaxLeafFormal.PDRate.hpd (↑m) MaxLeafFormal.PDRate.ystar ≤ MaxLeafFormal.PDRate.ωpr) ∧ 7050097 / 10 ^ 7 ≤ MaxLeafFormal.PDRate.ωpr ∧ MaxLeafFormal.PDRate.ωpr < 7050098 / 10 ^ 7 @MaxLeafFormal.RSCCert.C5_of_stages : ∀ {p₂ p₃ : ℝ}, 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1 → ∀ {Z : Finset (Fin 8 → ℝ)}, (∀ z ∈ Z, 0 ≤ z) → ∀ (P : Fin 8 → ℝ), 0 ≤ P → ∀ (j : ℕ) (Ys : ℕ → Finset (Fin 8 → ℝ)), Ys 0 = {P} → Ys j = Z → (∀ i < j, ∀ x ∈ Ys i, 0 ≤ x) → (∀ (i : ℕ), 1 ≤ i → i ≤ j → ∀ x ∈ Ys (i - 1), ∀ z ∈ Z, MaxLeafFormal.RSCCert.merge p₂ p₃ x z ∈ (convexHull ℝ) ↑(Ys i) + MaxLeafFormal.Antinorm8.Kpos) → ∀ (Qs : List (Fin 8 → ℝ)), Qs.length = j → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge p₂ p₃) P Qs ∈ MaxLeafFormal.Antinorm8.PZ Z MaxLeafFormal.RSCCert.certificate_conditions : ∀ (p₂ p₃ y ϖ₂ ϖ₃ ê : ℝ), 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1 / 2 → 0 < y → 1 ≤ ϖ₂ ∧ ϖ₂ ≤ 2 * (1 - p₂) ∧ 1 ≤ ϖ₃ ∧ ϖ₃ ≤ 2 * (1 - p₃) → 0 < ê ∧ ê < 1 - p₃ → ∀ (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → ∀ (ν₀ νE : ℕ), 1 ≤ νE → ∀ (d₃ d₂ : ℕ → ℕ), (∀ (ν : ℕ), 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge p₂ p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ ν₀, MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf p₂ y ∈ ê ^ (ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ νE → (∀ (d : ℕ), 1 ≤ d → d < d₃ ν → MaxLeafFormal.RSCCert.Light₃ p₂ p₃ y ν d) ∧ ∀ (d : ℕ), 1 ≤ d → d < d₂ ν → MaxLeafFormal.RSCCert.Light₂ p₂ p₃ y ν d) → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf d₃ ν else MaxLeafFormal.RSCCert.jOf d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1) → ∀ (t : MaxLeafFormal.Antinorm8.RTree MaxLeafFormal.RSCCert.Label), MaxLeafFormal.RSCCert.Admissible p₂ p₃ y t → MaxLeafFormal.Antinorm8.cZ p₂ Z hZ * ê ^ (MaxLeafFormal.Antinorm8.size t + MaxLeafFormal.RSCCert.nuSum t) ≤ MaxLeafFormal.Antinorm8.fin p₂ (MaxLeafFormal.RSCCert.message p₂ p₃ y ϖ₂ ϖ₃ t) MaxLeafFormal.RSCCert.certificate_conditions_of : ∀ (p₂ p₃ y ϖ₂ ϖ₃ ê : ℝ), 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1 / 2 → 0 < y → 1 ≤ ϖ₂ ∧ ϖ₂ ≤ 2 * (1 - p₂) ∧ 1 ≤ ϖ₃ ∧ ϖ₃ ≤ 2 * (1 - p₃) → 0 < ê ∧ ê < 1 - p₃ → ∀ (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → ∀ (ν₀ νE : ℕ), 1 ≤ νE → ∀ (d₃ d₂ : ℕ → ℕ), (∀ (ν : ℕ), 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν) → ∀ (L₂ L₃ : ℕ → ℕ → Prop), (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge p₂ p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ ν₀, MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf p₂ y ∈ ê ^ (ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ νE → (∀ (d : ℕ), 1 ≤ d → d < d₃ ν → L₃ ν d) ∧ ∀ (d : ℕ), 1 ≤ d → d < d₂ ν → L₂ ν d) → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf d₃ ν else MaxLeafFormal.RSCCert.jOf d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1) → ∀ (t : MaxLeafFormal.Antinorm8.RTree MaxLeafFormal.RSCCert.Label), MaxLeafFormal.RSCCert.AdmAt L₂ L₃ false t → MaxLeafFormal.Antinorm8.cZ p₂ Z hZ * ê ^ (MaxLeafFormal.Antinorm8.size t + MaxLeafFormal.RSCCert.nuSum t) ≤ MaxLeafFormal.Antinorm8.fin p₂ (MaxLeafFormal.RSCCert.message p₂ p₃ y ϖ₂ ϖ₃ t) MaxLeafFormal.RSCCert.rsc_cone_a : IsClosed MaxLeafFormal.Antinorm8.Kpos ∧ Convex ℝ MaxLeafFormal.Antinorm8.Kpos ∧ (∀ P ∈ MaxLeafFormal.Antinorm8.Kpos, ∀ Q ∈ MaxLeafFormal.Antinorm8.Kpos, P + Q ∈ MaxLeafFormal.Antinorm8.Kpos) ∧ (∀ (a : ℝ), 0 ≤ a → ∀ P ∈ MaxLeafFormal.Antinorm8.Kpos, a • P ∈ MaxLeafFormal.Antinorm8.Kpos) ∧ (∀ (P : Fin 8 → ℝ), 0 ≤ P → P ∈ MaxLeafFormal.Antinorm8.Kpos) ∧ ∀ (P : Fin 8 → ℝ), P ∈ MaxLeafFormal.Antinorm8.Kpos ↔ ∃ c, (∀ (i : Fin 14), 0 ≤ c i) ∧ P = ∑ i, c i • MaxLeafFormal.RSCCert.gen i @MaxLeafFormal.RSCCert.rsc_cone_b : ∀ {p₂ p₃ : ℝ}, 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1 → ∀ {Δ Q : Fin 8 → ℝ}, 0 ≤ Q → Δ ∈ MaxLeafFormal.Antinorm8.Kpos → MaxLeafFormal.RSCCert.merge p₂ p₃ Δ Q ∈ MaxLeafFormal.Antinorm8.Kpos ∧ MaxLeafFormal.RSCCert.merge p₂ p₃ Q Δ ∈ MaxLeafFormal.Antinorm8.Kpos @MaxLeafFormal.RSCCert.rsc_cone_c : ∀ {p₂ p₃ : ℝ}, 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1 → ∀ {Δ : Fin 8 → ℝ}, Δ ∈ MaxLeafFormal.Antinorm8.Kpos → 0 ≤ MaxLeafFormal.Antinorm8.fin p₂ Δ @MaxLeafFormal.RSCCompose.Wcl_eq : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (S : Finset V) (p₂ p₃ y : ℝ), MaxLeafFormal.RSCGraph.Wcl G S p₂ p₃ y = MaxLeafFormal.RSCTrials.Wcl G p₂ p₃ S y @MaxLeafFormal.RSCCompose.rsc_bound_trials : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ MaxLeafFormal.RSCParams.ν₀, MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 0 ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.y ∈ MaxLeafFormal.RSCParams.ê ^ (MaxLeafFormal.RSCParams.ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → MaxLeafFormal.RSCParams.d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (MaxLeafFormal.RSCParams.d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₃ ν else MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃) ((MaxLeafFormal.RSCParams.ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → 6060 / 10000 < MaxLeafFormal.Antinorm8.cZ MaxLeafFormal.RSCParams.p₂ Z hZ → ∀ (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → S.card = MaxLeafFormal.CDS.γc G → 0.6060 * (145729958 / 189014575) ^ Fintype.card V ≤ MaxLeafFormal.RSCTrials.Wcl G (7 / 100) (77 / 1000) S (31 / 100) @MaxLeafFormal.RSCCompose.rsc_maxLeaf_of_data : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ MaxLeafFormal.RSCParams.ν₀, MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 0 ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.y ∈ MaxLeafFormal.RSCParams.ê ^ (MaxLeafFormal.RSCParams.ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → MaxLeafFormal.RSCParams.d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (MaxLeafFormal.RSCParams.d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₃ ν else MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃) ((MaxLeafFormal.RSCParams.ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → 6060 / 10000 < MaxLeafFormal.Antinorm8.cZ MaxLeafFormal.RSCParams.p₂ Z hZ → ∀ (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (κ : ℝ), 0 < κ → ∀ (Θ : ℕ → ℕ), (∀ (s : ℕ), 1 ≤ s → s ≤ Fintype.card V → MaxLeafFormal.RSCTrials.rscOmega * ↑(Fintype.card V) + Real.logb 2 2 + 1 ≤ ↑(Θ s)) → ∀ (m : ℕ → ℕ → ℕ → ℕ), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s → MaxLeafFormal.Budget.Mcount (Fintype.card V) MaxLeafFormal.RSCTrials.rscOmega 2 κ (Θ s) θ ≤ ↑(m s t θ)) → 3 ≤ Fintype.card V → 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.cdsMeasure (Fintype.card V) (fun x t x_1 => MaxLeafFormal.RSCTrials.rscTrialMeasure G (7 / 100) (77 / 1000) t) Θ m).real {o | IsGreatest {ℓ | ∃ F ≤ G, F.IsTree ∧ MaxLeafFormal.CDS.numLeaves F = ℓ} (Fintype.card V - MaxLeafFormal.Budget.cdsOutput (Fintype.card V) (fun s x θ => MaxLeafFormal.RSCTrials.rscAccept G s θ) o)} MaxLeafFormal.RSCCompose.rsc_rho_lt : 16990 / 10000 < (1 + 31 / 100) / (145729958 / 189014575) ∧ (1 + 31 / 100) / (145729958 / 189014575) < 16991 / 10000 @MaxLeafFormal.RSCCompose.rsc_success_of_data : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ MaxLeafFormal.RSCParams.ν₀, MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 0 ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.y ∈ MaxLeafFormal.RSCParams.ê ^ (MaxLeafFormal.RSCParams.ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → MaxLeafFormal.RSCParams.d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (MaxLeafFormal.RSCParams.d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₃ ν else MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃) ((MaxLeafFormal.RSCParams.ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → 6060 / 10000 < MaxLeafFormal.Antinorm8.cZ MaxLeafFormal.RSCParams.p₂ Z hZ → ∀ (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (κ : ℝ), 0 < κ → ∀ (Θ : ℕ → ℕ), (∀ (s : ℕ), 1 ≤ s → s ≤ Fintype.card V → MaxLeafFormal.RSCTrials.rscOmega * ↑(Fintype.card V) + Real.logb 2 2 + 1 ≤ ↑(Θ s)) → ∀ (m : ℕ → ℕ → ℕ → ℕ), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s → MaxLeafFormal.Budget.Mcount (Fintype.card V) MaxLeafFormal.RSCTrials.rscOmega 2 κ (Θ s) θ ≤ ↑(m s t θ)) → (∀ (o : MaxLeafFormal.Budget.CdsOutcome (Fintype.card V) (fun x x_1 x_2 => Finset V × Finset V) Θ m), MaxLeafFormal.CDS.γc G ≤ MaxLeafFormal.Budget.cdsOutput (Fintype.card V) (fun s x θ => MaxLeafFormal.RSCTrials.rscAccept G s θ) o) ∧ 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.cdsMeasure (Fintype.card V) (fun x t x_1 => MaxLeafFormal.RSCTrials.rscTrialMeasure G (7 / 100) (77 / 1000) t) Θ m).real {o | MaxLeafFormal.Budget.cdsOutput (Fintype.card V) (fun s x θ => MaxLeafFormal.RSCTrials.rscAccept G s θ) o = MaxLeafFormal.CDS.γc G} @MaxLeafFormal.RSCGraph.EQ2 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 / 2 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → ∀ (u : MaxLeafFormal.RSCGraph.Out S), MaxLeafFormal.RSCGraph.Shared G S u → MaxLeafFormal.RSCGraph.typ G S u = 2 → ((MaxLeafFormal.RSCCert.delta₂ * MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X').Nonempty ∧ o u ∉ X' ∪ Υ) - MaxLeafFormal.RSCCert.eps P.p₂ * MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' _Υ => (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X').Nonempty ∧ o u ∈ X') ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htil P G S o u X' (X' ∪ Υ)) @MaxLeafFormal.RSCGraph.EQ3 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 / 2 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → ∀ (u : MaxLeafFormal.RSCGraph.Out S), MaxLeafFormal.RSCGraph.Shared G S u → MaxLeafFormal.RSCGraph.typ G S u = 3 → ((MaxLeafFormal.RSCCert.delta₃ P.p₃ * MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X').Nonempty ∧ o u ∉ X' ∪ Υ) - MaxLeafFormal.RSCCert.eps P.p₃ * MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X').Nonempty ∧ o u ∈ X' ∪ Υ) ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htil P G S o u X' (X' ∪ Υ)) @MaxLeafFormal.RSCGraph.EQex : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 / 2 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → ∀ u ∈ Oex, ((0 < MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => o u ∉ X' ∪ Υ) → (MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => o u ∉ X' ∪ Υ) * ((MaxLeafFormal.RSCGraph.deltaT P.p₃ (MaxLeafFormal.RSCGraph.typ G S u) * MaxLeafFormal.RSCTree.Pcond P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) (fun X' Υ => (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ (X' ∪ Υ)).Nonempty) fun X' Υ => o u ∉ X' ∪ Υ) - Real.log (MaxLeafFormal.RSCGraph.ϖT P (MaxLeafFormal.RSCGraph.typ G S u))) ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htilEx P G S o u X' (X' ∪ Υ))) ∧ ((MaxLeafFormal.RSCTree.Ptm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => o u ∉ X' ∪ Υ) = 0 → 0 ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htilEx P G S o u X' (X' ∪ Υ))) @MaxLeafFormal.RSCGraph.exists_ownerOK : ∀ {V : Type u_1} [Fintype V] [inst : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∃ o, (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) ∧ MaxLeafFormal.RSCGraph.OwnerOK G S F o @MaxLeafFormal.RSCGraph.rsc_bound_of_data : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ MaxLeafFormal.RSCParams.ν₀, MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 0 ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.y ∈ MaxLeafFormal.RSCParams.ê ^ (MaxLeafFormal.RSCParams.ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → MaxLeafFormal.RSCParams.d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (MaxLeafFormal.RSCParams.d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₃ ν else MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃) ((MaxLeafFormal.RSCParams.ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → ∀ (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → S.card = MaxLeafFormal.CDS.γc G → MaxLeafFormal.Antinorm8.cZ MaxLeafFormal.RSCParams.p₂ Z hZ * MaxLeafFormal.RSCParams.ê ^ Fintype.card V ≤ MaxLeafFormal.RSCGraph.Wcl G S MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y @MaxLeafFormal.RSCGraph.rsc_bound_of_data' : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty), (∀ z ∈ Z, 0 ≤ z) → (∀ z ∈ Z, ∀ z' ∈ Z, MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ z z' ∈ MaxLeafFormal.Antinorm8.PZ Z) → (∀ ν ≤ MaxLeafFormal.RSCParams.ν₀, MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 0 ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ MaxLeafFormal.Antinorm8.initInf MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.y ∈ MaxLeafFormal.RSCParams.ê ^ (MaxLeafFormal.RSCParams.ν₀ + 2) • MaxLeafFormal.Antinorm8.PZ Z → (∀ (ν : ℕ), 2 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → MaxLeafFormal.RSCParams.d₃ ν ≤ 1 → (∀ (c₃ : ℕ), 1 ≤ c₃ → c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν 0 c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z) ∧ (MaxLeafFormal.RSCParams.d₂ ν ≤ 1 → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 → MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃ ∈ MaxLeafFormal.RSCParams.ê ^ (1 + ν) • MaxLeafFormal.Antinorm8.PZ Z)) → (∀ (ν : ℕ), 1 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → ∀ (c₂ c₃ : ℕ), 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν → ∀ (Qs : List (Fin 8 → ℝ)), (Qs.length = if c₂ = 0 then MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₃ ν else MaxLeafFormal.RSCCert.jOf MaxLeafFormal.RSCParams.d₂ ν) → (∀ Q ∈ Qs, Q ∈ MaxLeafFormal.Antinorm8.PZ Z ∧ 0 ≤ Q) → List.foldl (MaxLeafFormal.RSCCert.merge MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃) ((MaxLeafFormal.RSCParams.ê ^ (1 + ν))⁻¹ • MaxLeafFormal.RSCCert.init MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ ν c₂ c₃) Qs ∈ MaxLeafFormal.Antinorm8.PZ Z) → 6060 / 10000 < MaxLeafFormal.Antinorm8.cZ MaxLeafFormal.RSCParams.p₂ Z hZ → ∀ (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → S.card = MaxLeafFormal.CDS.γc G → 6060 / 10000 * MaxLeafFormal.RSCParams.ê ^ Fintype.card V ≤ MaxLeafFormal.RSCGraph.Wcl G S MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y @MaxLeafFormal.RSCGraph.rsc_credit : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), P.Standing → ∀ u ∈ Oex, (if MaxLeafFormal.RSCGraph.typ G S u = 2 then 1 - MaxLeafFormal.RSCCert.rho₁ P.p₃ P.y else 1 - MaxLeafFormal.RSCCert.rho₁ P.p₃ P.y ^ 2) ≤ MaxLeafFormal.RSCTree.Pcond P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) (fun X' Υ => (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ (X' ∪ Υ)).Nonempty) fun X' Υ => o u ∉ X' ∪ Υ @MaxLeafFormal.RSCGraph.rsc_credit_ex : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), P.Standing → MaxLeafFormal.RSCCert.Credits P.p₃ P.y P.ϖ₂ P.ϖ₃ → ∀ u ∈ Oex, 0 ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htilEx P G S o u X' (X' ∪ Υ)) @MaxLeafFormal.RSCGraph.rsc_jensen : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 / 2 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → MaxLeafFormal.RSCTree.Wtm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) * Real.exp ((∑ u ∈ MaxLeafFormal.RSCGraph.Oco G S Oex, MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htil P G S o u X' (X' ∪ Υ))) + ∑ u ∈ Oex, MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htilEx P G S o u X' (X' ∪ Υ))) ≤ MaxLeafFormal.RSCGraph.Wcl G S P.p₂ P.p₃ P.y @MaxLeafFormal.RSCGraph.rsc_jensen_nonneg : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 / 2 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → (∀ u ∈ MaxLeafFormal.RSCGraph.Oco G S Oex, 0 ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htil P G S o u X' (X' ∪ Υ))) → (∀ u ∈ Oex, 0 ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htilEx P G S o u X' (X' ∪ Υ))) → MaxLeafFormal.RSCTree.Wtm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) ≤ MaxLeafFormal.RSCGraph.Wcl G S P.p₂ P.p₃ P.y @MaxLeafFormal.RSCGraph.rsc_jlemma : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (Oex : Finset (MaxLeafFormal.RSCGraph.Out S)), (∀ u ∈ Oex, MaxLeafFormal.RSCGraph.Shared G S u) → ∀ (P : MaxLeafFormal.RSCRec.Par), P.Standing → ∀ (u : MaxLeafFormal.RSCGraph.Out S), MaxLeafFormal.RSCGraph.Shared G S u → MaxLeafFormal.RSCGraph.LightT P (MaxLeafFormal.RSCGraph.typ G S u) (MaxLeafFormal.RSCGraph.nuOf o (o u)) (F.degree (o u)) → MaxLeafFormal.RSCGraph.IsLeafIn F (MaxLeafFormal.RSCGraph.span F (MaxLeafFormal.RSCGraph.NS G S u)) (o u) → 0 ≤ MaxLeafFormal.RSCTree.Etm P F (MaxLeafFormal.RSCGraph.labOf G S o Oex) fun X' Υ => Real.log (MaxLeafFormal.RSCGraph.htil P G S o u X' (X' ∪ Υ)) @MaxLeafFormal.RSCGraph.rsc_leaf : ∀ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → S.card = MaxLeafFormal.CDS.γc G → 2 ≤ S.card → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (v : ↥S), F.degree v = 1 → ∃ u, MaxLeafFormal.RSCGraph.NS G S u = {v} @MaxLeafFormal.RSCGraph.rsc_model : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (p₂ p₃ y : ℝ), 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 → 0 ≤ y → ∑ X', ∑ Υ ∈ (MaxLeafFormal.RSCTree.candF F X').powerset, y ^ X'.card * MaxLeafFormal.RSCTree.piF p₂ p₃ F X' Υ * (1 / 2) ^ MaxLeafFormal.RSCTree.psiF F (X' ∪ Υ) * ∏ u, MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' (X' ∪ Υ) ≤ MaxLeafFormal.RSCGraph.Wcl G S p₂ p₃ y @MaxLeafFormal.RSCGraph.rsc_mono : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] {X Y : Finset V}, X ⊆ Y → MaxLeafFormal.CDS.termCount G Y ≤ MaxLeafFormal.CDS.termCount G X @MaxLeafFormal.RSCGraph.rsc_pointwise : ∀ {V : Type u_1} [Fintype V] [inst : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (p₂ p₃ : ℝ), 0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1 / 2 → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → ∀ (u : MaxLeafFormal.RSCGraph.Out S) {X' X : Finset ↥S}, X' ⊆ X → (o u ∉ X → MaxLeafFormal.RSCGraph.hbar o u X ≤ MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' X) ∧ (MaxLeafFormal.RSCGraph.Private G S u → MaxLeafFormal.RSCGraph.hbar o u X ≤ MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' X) ∧ (MaxLeafFormal.RSCGraph.Shared G S u → (MaxLeafFormal.RSCGraph.hbar o u X * MaxLeafFormal.RSCGraph.qT p₂ p₃ (MaxLeafFormal.RSCGraph.typ G S u) ^ if o u ∈ X then 1 else 0) ≤ MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' X) ∧ (MaxLeafFormal.RSCGraph.Shared G S u → o u ∉ X → (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X).Nonempty → Real.exp (MaxLeafFormal.RSCGraph.deltaT p₃ (MaxLeafFormal.RSCGraph.typ G S u)) * MaxLeafFormal.RSCGraph.hbar o u X ≤ MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' X) ∧ (MaxLeafFormal.RSCGraph.Shared G S u → MaxLeafFormal.RSCGraph.typ G S u = 3 → MaxLeafFormal.RSCGraph.ind (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X').Nonempty * (MaxLeafFormal.RSCCert.delta₃ p₃ * MaxLeafFormal.RSCGraph.ind (o u ∉ X) - MaxLeafFormal.RSCCert.eps p₃ * MaxLeafFormal.RSCGraph.ind (o u ∈ X)) ≤ Real.log (MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' X / MaxLeafFormal.RSCGraph.hbar o u X)) ∧ (MaxLeafFormal.RSCGraph.Shared G S u → MaxLeafFormal.RSCGraph.typ G S u = 2 → MaxLeafFormal.RSCGraph.ind (MaxLeafFormal.RSCGraph.Nprime G S o u ∩ X').Nonempty * (MaxLeafFormal.RSCCert.delta₂ * MaxLeafFormal.RSCGraph.ind (o u ∉ X) - MaxLeafFormal.RSCCert.eps p₂ * MaxLeafFormal.RSCGraph.ind (o u ∈ X')) ≤ Real.log (MaxLeafFormal.RSCGraph.hfac p₂ p₃ G S u X' X / MaxLeafFormal.RSCGraph.hbar o u X)) @MaxLeafFormal.RSCGraph.rsc_reduction : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (P : MaxLeafFormal.RSCRec.Par), P.Standing → MaxLeafFormal.RSCCert.Credits P.p₃ P.y P.ϖ₂ P.ϖ₃ → S.card = MaxLeafFormal.CDS.γc G → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → MaxLeafFormal.RSCGraph.OwnerRule G S F o → MaxLeafFormal.RSCTree.AdmissibleG P F (MaxLeafFormal.RSCGraph.labOf G S o (MaxLeafFormal.RSCGraph.OexRule P G S F o)) ∧ S.card + ∑ v, MaxLeafFormal.RSCGraph.nuOf o v = Fintype.card V ∧ MaxLeafFormal.RSCTree.Wtm P F (MaxLeafFormal.RSCGraph.labOf G S o (MaxLeafFormal.RSCGraph.OexRule P G S F o)) ≤ MaxLeafFormal.RSCGraph.Wcl G S P.p₂ P.p₃ P.y @MaxLeafFormal.RSCGraph.rsc_reduction_of : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ F ≤ SimpleGraph.induce (↑S) G, F.IsTree → ∀ (P : MaxLeafFormal.RSCRec.Par), P.Standing → MaxLeafFormal.RSCCert.Credits P.p₃ P.y P.ϖ₂ P.ϖ₃ → S.card = MaxLeafFormal.CDS.γc G → ∀ (o : MaxLeafFormal.RSCGraph.Out S → ↥S), (∀ (u : MaxLeafFormal.RSCGraph.Out S), G.Adj ↑u ↑(o u)) → MaxLeafFormal.RSCGraph.OwnerOK G S F o → MaxLeafFormal.RSCTree.AdmissibleG P F (MaxLeafFormal.RSCGraph.labOf G S o (MaxLeafFormal.RSCGraph.OexRule P G S F o)) ∧ S.card + ∑ v, MaxLeafFormal.RSCGraph.nuOf o v = Fintype.card V ∧ MaxLeafFormal.RSCTree.Wtm P F (MaxLeafFormal.RSCGraph.labOf G S o (MaxLeafFormal.RSCGraph.OexRule P G S F o)) ≤ MaxLeafFormal.RSCGraph.Wcl G S P.p₂ P.p₃ P.y MaxLeafFormal.RSCParams.rsc_C3 : ∀ (ν : ℕ), 1 ≤ ν → ν ≤ MaxLeafFormal.RSCParams.νE → (∀ (d : ℕ), 1 ≤ d → d < MaxLeafFormal.RSCParams.d₃ ν → MaxLeafFormal.RSCCert.Light₃ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y ν d) ∧ ∀ (d : ℕ), 1 ≤ d → d < MaxLeafFormal.RSCParams.d₂ ν → MaxLeafFormal.RSCCert.Light₂ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y ν d MaxLeafFormal.RSCParams.rsc_lightpairs : MaxLeafFormal.RSCCert.Light₃ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y 1 1 ∧ MaxLeafFormal.RSCCert.Light₃ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y 1 2 ∧ MaxLeafFormal.RSCCert.Light₃ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y 2 1 ∧ MaxLeafFormal.RSCCert.Light₃ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y 3 1 ∧ MaxLeafFormal.RSCCert.Light₂ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y 1 3 ∧ MaxLeafFormal.RSCCert.Light₂ MaxLeafFormal.RSCParams.p₂ MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y 2 2 MaxLeafFormal.RSCParams.rsc_rsccredits : (1 ≤ MaxLeafFormal.RSCParams.ϖ₂ ∧ MaxLeafFormal.RSCParams.ϖ₂ ≤ 2 * (1 - MaxLeafFormal.RSCParams.p₂) ∧ 1 ≤ MaxLeafFormal.RSCParams.ϖ₃ ∧ MaxLeafFormal.RSCParams.ϖ₃ ≤ 2 * (1 - MaxLeafFormal.RSCParams.p₃)) ∧ MaxLeafFormal.RSCCert.Credits MaxLeafFormal.RSCParams.p₃ MaxLeafFormal.RSCParams.y MaxLeafFormal.RSCParams.ϖ₂ MaxLeafFormal.RSCParams.ϖ₃ MaxLeafFormal.RSCRec.rsc_messages : ∀ (P : MaxLeafFormal.RSCRec.Par), P.Standing → ∀ (t : MaxLeafFormal.Antinorm8.RTree MaxLeafFormal.RSCRec.FLabel), MaxLeafFormal.RSCRec.AllLabels (fun a => a.1.2.1 + a.1.2.2 ≤ a.1.1) t → have M := MaxLeafFormal.RSCRec.message10 P t; (MaxLeafFormal.RSCRec.forcing t ≠ some MaxLeafFormal.RSCRec.Force.excl → P.p₂ / 2 * (M 5 + M 6) ≤ M 1 ∧ P.p₂ / 2 * M 7 ≤ M 2 ∧ P.p₂ / 2 * M 8 ≤ M 3 ∧ P.p₂ / 2 * M 9 ≤ M 4) ∧ (MaxLeafFormal.RSCRec.forcing t ≠ some MaxLeafFormal.RSCRec.Force.out → (∀ c ∈ MaxLeafFormal.RSCRec.kids t, MaxLeafFormal.RSCRec.forcing c ≠ some MaxLeafFormal.RSCRec.Force.excl) → M 1 + M 2 + M 3 + M 4 ≤ P.p₂ / P.y * M 0) ∧ (MaxLeafFormal.RSCRec.forcing t ≠ some MaxLeafFormal.RSCRec.Force.out → (∀ c ∈ MaxLeafFormal.RSCRec.kids t, MaxLeafFormal.RSCRec.forcing c ≠ some MaxLeafFormal.RSCRec.Force.excl) → MaxLeafFormal.RSCRec.chiS10 P M ≤ MaxLeafFormal.RSCCert.bconst P.p₂ P.p₃ P.y * MaxLeafFormal.RSCRec.chiO10 P M) ∧ (MaxLeafFormal.RSCRec.forcing t ≠ some MaxLeafFormal.RSCRec.Force.excl → MaxLeafFormal.RSCRec.chiO10 P M ≤ MaxLeafFormal.RSCRec.chiS10 P M) ∧ (MaxLeafFormal.RSCRec.forcing t = some MaxLeafFormal.RSCRec.Force.excl → (1 - P.p₃) * MaxLeafFormal.RSCRec.chiO10 P M ≤ MaxLeafFormal.RSCRec.chiS10 P M) @MaxLeafFormal.RSCTree.monotone_coupling : ∀ {α : Type u_1} [inst : DecidableEq α] (C : Finset α) (f : Finset α → ℝ), (∀ Υ ⊆ C, 0 ≤ f Υ) → (∀ (Υ Υ' : Finset α), Υ ⊆ Υ' → Υ' ⊆ C → f Υ ≤ f Υ') → ∀ (p p' : α → ℝ), (∀ v ∈ C, 0 ≤ p v ∧ p v ≤ p' v ∧ p' v ≤ 1) → ∑ Υ ∈ C.powerset, MaxLeafFormal.RSCTree.prodMeas p C Υ * f Υ ≤ ∑ Υ ∈ C.powerset, MaxLeafFormal.RSCTree.prodMeas p' C Υ * f Υ @MaxLeafFormal.RSCTree.odds1 : ∀ {Vt : Type u_1} [inst : Fintype Vt] [inst_1 : DecidableEq Vt] (P : MaxLeafFormal.RSCRec.Par), P.Standing → ∀ {F : SimpleGraph Vt}, F.IsTree → ∀ (lab : Vt → MaxLeafFormal.RSCCert.Label), (∀ (v : Vt), (lab v).2.1 + (lab v).2.2 ≤ (lab v).1) → ∀ (o w : Vt), w ≠ o → (MaxLeafFormal.RSCTree.Pcond P F lab (fun X' Υ => w ∉ X' ∪ Υ) fun X' Υ => o ∉ X' ∪ Υ) ≤ MaxLeafFormal.RSCCert.rho₁ P.p₃ P.y @MaxLeafFormal.RSCTree.rsc_odds : ∀ {Vt : Type u_1} [inst : Fintype Vt] [inst_1 : DecidableEq Vt] (P : MaxLeafFormal.RSCRec.Par), P.Standing → ∀ {F : SimpleGraph Vt}, F.IsTree → ∀ (lab : Vt → MaxLeafFormal.RSCCert.Label), (∀ (v : Vt), (lab v).2.1 + (lab v).2.2 ≤ (lab v).1) → ∀ (U : Finset Vt), ∀ w ∉ U, (Finset.filter (F.Adj w) U).card ≤ 1 → (P.y / 2 * (1 - P.p₃) ^ (Finset.filter (F.Adj w) U).card * MaxLeafFormal.RSCTree.Ptm P F lab fun X' Υ => Disjoint U (X' ∪ Υ) ∧ w ∉ X' ∪ Υ) ≤ MaxLeafFormal.RSCTree.Ptm P F lab fun X' Υ => Disjoint U (X' ∪ Υ) ∧ w ∈ X' @MaxLeafFormal.RSCTree.rsc_recursion : ∀ {Vt : Type u_1} [inst : Fintype Vt] [inst_1 : DecidableEq Vt] (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → ∀ {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (ord : Vt → List Vt), MaxLeafFormal.RSCTree.IsChildOrder hF r ord → ∀ (lab : Vt → MaxLeafFormal.RSCCert.Label) (f : Vt → Option MaxLeafFormal.RSCRec.Force), have M := MaxLeafFormal.RSCRec.message10 P (MaxLeafFormal.RSCTree.toRTree hF r ord (fun v => (lab v, f v)) r); (∀ (v : Vt), 0 ≤ MaxLeafFormal.RSCRec.message10 P (MaxLeafFormal.RSCTree.toRTree hF r ord (fun v => (lab v, f v)) v)) ∧ (M 0 = MaxLeafFormal.RSCTree.wsum P F lab fun X' Υ => MaxLeafFormal.RSCTree.Respects f X' Υ ∧ r ∈ X') ∧ (M 3 + MaxLeafFormal.RSCRec.lam P * M 4 = MaxLeafFormal.RSCTree.wsum P F lab fun X' Υ => MaxLeafFormal.RSCTree.Respects f X' Υ ∧ r ∈ Υ) ∧ M 5 / 2 + M 6 + M 7 + (1 - P.p₂) * M 8 + (1 - P.p₃) * M 9 = MaxLeafFormal.RSCTree.wsum P F lab fun X' Υ => MaxLeafFormal.RSCTree.Respects f X' Υ ∧ r ∉ X' ∪ Υ @MaxLeafFormal.RSCTree.rsc_recursion_fin : ∀ {Vt : Type u_1} [inst : Fintype Vt] [inst_1 : DecidableEq Vt] (P : MaxLeafFormal.RSCRec.Par), 0 < P.p₂ ∧ P.p₂ ≤ P.p₃ ∧ P.p₃ < 1 → 0 ≤ P.y → 1 ≤ P.ϖ₂ ∧ 1 ≤ P.ϖ₃ → ∀ {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (ord : Vt → List Vt), MaxLeafFormal.RSCTree.IsChildOrder hF r ord → ∀ (lab : Vt → MaxLeafFormal.RSCCert.Label) (f : Vt → Option MaxLeafFormal.RSCRec.Force), (MaxLeafFormal.RSCRec.fin10 P (MaxLeafFormal.RSCRec.message10 P (MaxLeafFormal.RSCTree.toRTree hF r ord (fun v => (lab v, f v)) r)) = MaxLeafFormal.RSCTree.wsum P F lab fun X' Υ => MaxLeafFormal.RSCTree.Respects f X' Υ) ∧ ((∀ (v : Vt), f v = none) → MaxLeafFormal.RSCRec.fin10 P (MaxLeafFormal.RSCRec.message10 P (MaxLeafFormal.RSCTree.toRTree hF r ord (fun v => (lab v, f v)) r)) = MaxLeafFormal.RSCTree.Wtm P F lab) @MaxLeafFormal.RSCTree.rsc_relaxed : ∀ {Vt : Type u_1} [inst : Fintype Vt] [inst_1 : DecidableEq Vt] (P : MaxLeafFormal.RSCRec.Par), P.Standing → ∀ {F : SimpleGraph Vt} (hF : F.IsTree) (r : Vt) (ord : Vt → List Vt), MaxLeafFormal.RSCTree.IsChildOrder hF r ord → ∀ (lab : Vt → MaxLeafFormal.RSCCert.Label), (∀ (v : Vt), (lab v).2.1 + (lab v).2.2 ≤ (lab v).1) → MaxLeafFormal.RSCTree.Wrel P hF r lab ≤ MaxLeafFormal.RSCTree.Wtm P F lab ∧ MaxLeafFormal.RSCTree.Wrel P hF r lab = MaxLeafFormal.Antinorm8.fin P.p₂ (MaxLeafFormal.RSCCert.message P.p₂ P.p₃ P.y P.ϖ₂ P.ϖ₃ (MaxLeafFormal.RSCTree.toRTree hF r ord lab r)) @MaxLeafFormal.RSCTrials.rsc_success_of_bound : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (κ : ℝ), 0 < κ → ∀ (Θ : ℕ → ℕ), (∀ (s : ℕ), 1 ≤ s → s ≤ Fintype.card V → MaxLeafFormal.RSCTrials.rscOmega * ↑(Fintype.card V) + Real.logb 2 2 + 1 ≤ ↑(Θ s)) → ∀ (m : ℕ → ℕ → ℕ → ℕ), (∀ (s t θ : ℕ), 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s → MaxLeafFormal.Budget.Mcount (Fintype.card V) MaxLeafFormal.RSCTrials.rscOmega 2 κ (Θ s) θ ≤ ↑(m s t θ)) → (∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → S.card = MaxLeafFormal.CDS.γc G → 0.6060 * (145729958 / 189014575) ^ Fintype.card V ≤ MaxLeafFormal.RSCTrials.Wcl G (7 / 100) (77 / 1000) S (31 / 100)) → (∀ (o : MaxLeafFormal.Budget.CdsOutcome (Fintype.card V) (fun x x_1 x_2 => Finset V × Finset V) Θ m), MaxLeafFormal.CDS.γc G ≤ MaxLeafFormal.Budget.cdsOutput (Fintype.card V) (fun s x θ => MaxLeafFormal.RSCTrials.rscAccept G s θ) o) ∧ 1 - Real.exp (-κ) ≤ (MaxLeafFormal.Budget.cdsMeasure (Fintype.card V) (fun x t x_1 => MaxLeafFormal.RSCTrials.rscTrialMeasure G (7 / 100) (77 / 1000) t) Θ m).real {o | MaxLeafFormal.Budget.cdsOutput (Fintype.card V) (fun s x θ => MaxLeafFormal.RSCTrials.rscAccept G s θ) o = MaxLeafFormal.CDS.γc G} @MaxLeafFormal.RSCTrials.rsc_trials_T2 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (s θ : ℕ), ∀ z ∈ MaxLeafFormal.RSCTrials.rscAccept G s θ, MaxLeafFormal.CDS.γc G ≤ s @MaxLeafFormal.RSCTrials.rsc_trials_T3 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (p₂ p₃ : ℝ), 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → ∀ (t θ : ℕ), (MaxLeafFormal.RSCTrials.rscTrialMeasure G p₂ p₃ t).real (MaxLeafFormal.Budget.leEvent (MaxLeafFormal.RSCTrials.xi G S) ↑θ) ≤ (MaxLeafFormal.RSCTrials.rscTrialMeasure G p₂ p₃ t).real (MaxLeafFormal.RSCTrials.rscAccept G S.card θ) @MaxLeafFormal.RSCTrials.rsc_trials_W : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (p₂ p₃ : ℝ), 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1 → ∀ (S : Finset V) (y : ℝ), 0 ≤ y → ∃ t ≤ S.card, MaxLeafFormal.RSCTrials.Wcl G p₂ p₃ S y ≤ (1 + y) ^ Fintype.card V * ∫ (z : Finset V × Finset V), MaxLeafFormal.Budget.twoPowNeg (MaxLeafFormal.RSCTrials.xi G S z) ∂MaxLeafFormal.RSCTrials.rscTrialMeasure G p₂ p₃ t @MaxLeafFormal.RSRate.rsF_eq_Fstar : ∀ {σ : ℝ}, σ ∈ Set.Ioo 0 1 → MaxLeafFormal.RSRate.rsF σ = MaxLeafFormal.MLS.Fstar σ 1 σ⁻¹ MaxLeafFormal.RSRate.rsF_one : MaxLeafFormal.RSRate.rsF 1 = 0 MaxLeafFormal.RSRate.rs_constants : Real.logb 2 (1744835 / 10 ^ 6) < 80309062 / 10 ^ 8 ∧ 1744835 / 10 ^ 6 ≤ 2 ^ (80309062 / 10 ^ 8) ∧ 2 ^ (80309062 / 10 ^ 8) < 1744836 / 10 ^ 6 MaxLeafFormal.RSRate.rs_rate_c : (∀ σ ∈ Set.Ioc 0 1, MaxLeafFormal.RSRate.rsF σ ≤ Real.logb 2 (1744835 / 10 ^ 6)) ∧ (∀ σ ∈ Set.Ioc 0 (31 / 100), MaxLeafFormal.RSRate.rsF σ ≤ 7807 / 10 ^ 4) ∧ ∀ σ ∈ Set.Icc (54 / 100) 1, MaxLeafFormal.RSRate.rsF σ ≤ 7802 / 10 ^ 4 @MaxLeafFormal.RSRateAB.rsTau_eq_τstar : ∀ {σ : ℝ}, σ ∈ Set.Ioo 0 1 → MaxLeafFormal.RSRateAB.rsTau σ = MaxLeafFormal.MLS.τstar σ σ⁻¹ @MaxLeafFormal.RSRateAB.rs_base : ∀ {σ : ℝ}, σ ∈ Set.Ioo 0 1 → 2 ^ MaxLeafFormal.RSRate.rsF σ = (1 - 2 ^ (-1 / σ)) ^ (1 - σ) / (σ ^ σ * (1 - σ) ^ (1 - σ)) @MaxLeafFormal.RSRateAB.rs_base_denom : ∀ {σ : ℝ}, σ ∈ Set.Ioo 0 1 → σ ^ σ * (1 - σ) ^ (1 - σ) = 2 ^ (-MaxLeafFormal.MLS.H2 σ) @MaxLeafFormal.RSRateAB.rs_rate_a : ∀ {σ : ℝ}, σ ∈ Set.Ioo 0 1 → MaxLeafFormal.RSRate.rsF σ < MaxLeafFormal.MLS.H2 σ ∧ MaxLeafFormal.MLS.H2 σ ≤ 1 ∧ MaxLeafFormal.RSRateAB.rsTau σ ∈ Set.Ioo 0 σ ∧ (∀ τ ∈ Set.Icc 0 σ, MaxLeafFormal.RSRateAB.rsfσ σ (MaxLeafFormal.RSRateAB.rsTau σ) ≤ MaxLeafFormal.RSRateAB.rsfσ σ τ) ∧ ∀ τ ∈ Set.Icc 0 σ, MaxLeafFormal.RSRateAB.rsfσ σ τ = MaxLeafFormal.RSRateAB.rsfσ σ (MaxLeafFormal.RSRateAB.rsTau σ) → τ = MaxLeafFormal.RSRateAB.rsTau σ MaxLeafFormal.RSRateAB.rs_rate_b : MaxLeafFormal.RSRateAB.rsTau (1 / 2) = 1 / 3 ∧ MaxLeafFormal.RSRate.rsF (1 / 2) = Real.logb 2 3 / 2 ∧ 2 ^ MaxLeafFormal.RSRate.rsF (1 / 2) = √3 MaxLeafFormal.RSRateAB.rs_rate_b_argmin : 1 / 3 ∈ Set.Icc 0 (1 / 2) ∧ (∀ τ ∈ Set.Icc 0 (1 / 2), MaxLeafFormal.RSRateAB.rsfσ (1 / 2) (1 / 3) ≤ MaxLeafFormal.RSRateAB.rsfσ (1 / 2) τ) ∧ ∀ τ ∈ Set.Icc 0 (1 / 2), MaxLeafFormal.RSRateAB.rsfσ (1 / 2) τ = MaxLeafFormal.RSRateAB.rsfσ (1 / 2) (1 / 3) → τ = 1 / 3 MaxLeafFormal.RSRateAB.rsfσ_eq_fσ : ∀ (σ : ℝ), MaxLeafFormal.RSRateAB.rsfσ σ = MaxLeafFormal.MLS.fσ σ 1 σ⁻¹ @MaxLeafFormal.RSRateAB.rsfσ_min_eq : ∀ {σ : ℝ}, σ ∈ Set.Ioo 0 1 → MaxLeafFormal.RSRateAB.rsfσ σ (MaxLeafFormal.RSRateAB.rsTau σ) = MaxLeafFormal.RSRate.rsF σ MaxLeafFormal.RSThetaCert.cert0_Z : MaxLeafFormal.Antinorm3.checkZ MaxLeafFormal.RSThetaCert.Z0 (MaxLeafFormal.RSThetaCert.q 6212 10000) = true MaxLeafFormal.RSThetaCert.cert0_inits : MaxLeafFormal.Antinorm3.checkInits MaxLeafFormal.RSThetaCert.Z0 MaxLeafFormal.RSThetaCert.y0 MaxLeafFormal.RSThetaCert.e1_0 MaxLeafFormal.RSThetaCert.e2_0 MaxLeafFormal.RSThetaCert.m0_0 MaxLeafFormal.RSThetaCert.inits0 MaxLeafFormal.RSThetaCert.tail0 = true MaxLeafFormal.RSThetaCert.cert0_pairs : MaxLeafFormal.Antinorm3.checkPairs MaxLeafFormal.RSThetaCert.Z0 MaxLeafFormal.RSThetaCert.pairs0 = true MaxLeafFormal.RSThetaCert.cert1_Z : MaxLeafFormal.Antinorm3.checkZ MaxLeafFormal.RSThetaCert.Z1 (MaxLeafFormal.RSThetaCert.q 6293 10000) = true MaxLeafFormal.RSThetaCert.cert1_inits : MaxLeafFormal.Antinorm3.checkInits MaxLeafFormal.RSThetaCert.Z1 MaxLeafFormal.RSThetaCert.y1 MaxLeafFormal.RSThetaCert.e1_1 MaxLeafFormal.RSThetaCert.e2_1 MaxLeafFormal.RSThetaCert.m0_1 MaxLeafFormal.RSThetaCert.inits1 MaxLeafFormal.RSThetaCert.tail1 = true MaxLeafFormal.RSThetaCert.cert1_pairs : MaxLeafFormal.Antinorm3.checkPairs MaxLeafFormal.RSThetaCert.Z1 MaxLeafFormal.RSThetaCert.pairs1 = true MaxLeafFormal.RSThetaRate.rst_rates : (∀ σ ∈ Set.Icc (31 / 100) (4172629 / 10 ^ 7), MaxLeafFormal.RSThetaRate.ω₀ σ < 78270152 / 10 ^ 8) ∧ (∀ σ ∈ Set.Icc (4172629 / 10 ^ 7) (54 / 100), MaxLeafFormal.RSThetaRate.ω₁ σ < 78270152 / 10 ^ 8) ∧ 78270152 / 10 ^ 8 < 7827016 / 10 ^ 7 ∧ 7807 / 10000 < 7827016 / 10 ^ 7 ∧ MaxLeafFormal.MLS.H2 (1 / 5) < 7802 / 10000 ∧ 17203 / 10 ^ 4 ≤ 2 ^ (7827016 / 10 ^ 7) ∧ 2 ^ (7827016 / 10 ^ 7) < 17204 / 10 ^ 4 MaxLeafFormal.RSThetaRate.rst_rates_detail : |MaxLeafFormal.RSThetaRate.a0 ↑MaxLeafFormal.RSThetaCert.y0 ↑MaxLeafFormal.RSThetaCert.e2_0 - 7776061742 / 10 ^ 10| ≤ 1 / (2 * 10 ^ 10) ∧ |MaxLeafFormal.RSThetaRate.a1 ↑MaxLeafFormal.RSThetaCert.e1_0 ↑MaxLeafFormal.RSThetaCert.e2_0 - 122113367 / 10 ^ 10| ≤ 1 / (2 * 10 ^ 10) ∧ |MaxLeafFormal.RSThetaRate.a0 ↑MaxLeafFormal.RSThetaCert.y1 ↑MaxLeafFormal.RSThetaCert.e2_1 - 8022330021 / 10 ^ 10| ≤ 1 / (2 * 10 ^ 10) ∧ |MaxLeafFormal.RSThetaRate.a1 ↑MaxLeafFormal.RSThetaCert.e1_1 ↑MaxLeafFormal.RSThetaCert.e2_1 - -468085913 / 10 ^ 10| ≤ 1 / (2 * 10 ^ 10) ∧ 4172629270 / 10 ^ 10 ≤ (MaxLeafFormal.RSThetaRate.a0 ↑MaxLeafFormal.RSThetaCert.y1 ↑MaxLeafFormal.RSThetaCert.e2_1 - MaxLeafFormal.RSThetaRate.a0 ↑MaxLeafFormal.RSThetaCert.y0 ↑MaxLeafFormal.RSThetaCert.e2_0) / (MaxLeafFormal.RSThetaRate.a1 ↑MaxLeafFormal.RSThetaCert.e1_0 ↑MaxLeafFormal.RSThetaCert.e2_0 - MaxLeafFormal.RSThetaRate.a1 ↑MaxLeafFormal.RSThetaCert.e1_1 ↑MaxLeafFormal.RSThetaCert.e2_1) ∧ (MaxLeafFormal.RSThetaRate.a0 ↑MaxLeafFormal.RSThetaCert.y1 ↑MaxLeafFormal.RSThetaCert.e2_1 - MaxLeafFormal.RSThetaRate.a0 ↑MaxLeafFormal.RSThetaCert.y0 ↑MaxLeafFormal.RSThetaCert.e2_0) / (MaxLeafFormal.RSThetaRate.a1 ↑MaxLeafFormal.RSThetaCert.e1_0 ↑MaxLeafFormal.RSThetaCert.e2_0 - MaxLeafFormal.RSThetaRate.a1 ↑MaxLeafFormal.RSThetaCert.e1_1 ↑MaxLeafFormal.RSThetaCert.e2_1) < 4172629271 / 10 ^ 10 ∧ ∃ m, IsGreatest (MaxLeafFormal.RSThetaRate.ω₀ '' Set.Icc (31 / 100) (4172629 / 10 ^ 7) ∪ MaxLeafFormal.RSThetaRate.ω₁ '' Set.Icc (4172629 / 10 ^ 7) (54 / 100)) m ∧ 78270151357 / 10 ^ 11 ≤ m ∧ m < 78270151358 / 10 ^ 11 @MaxLeafFormal.RateAssembly.rs_moments : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → MaxLeafFormal.MLS.Star (MaxLeafFormal.RateAssembly.gT G) S S.card (MaxLeafFormal.RSRate.rsF (↑S.card / ↑(Fintype.card V))) 2 @MaxLeafFormal.RateAssembly.rs_star : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → MaxLeafFormal.MLS.Star (MaxLeafFormal.RateAssembly.gT G) S S.card (80309062 / 10 ^ 8) 2 @MaxLeafFormal.RateAssembly.rst_rate : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → ∀ (S : Finset V), MaxLeafFormal.CDS.IsCDS G S → MaxLeafFormal.MLS.Star (MaxLeafFormal.RateAssembly.gT G) S S.card (7827016 / 10 ^ 7) 2 @MaxLeafFormal.SteinerCDS.aSt_iff_ext : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (X : Finset V) (k : ℕ), MaxLeafFormal.SteinerCDS.aSt G X k ↔ ∃ Y, Disjoint X Y ∧ X.card + Y.card ≤ k ∧ MaxLeafFormal.CDS.IsCDS G (X ∪ Y) @MaxLeafFormal.SteinerCDS.aSt_iff_extYes : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (X : Finset V) (k : ℕ), X.card ≤ k → (MaxLeafFormal.SteinerCDS.aSt G X k ↔ MaxLeafFormal.MLS.ExtYes (MaxLeafFormal.CDS.IsCDS G) X (k - X.card)) @MaxLeafFormal.SteinerCDS.isSol_JX_iff : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (X Y : Finset V), MaxLeafFormal.SteinerCDS.IsSol G (MaxLeafFormal.SteinerCDS.JX G X) Y ↔ Disjoint X Y ∧ MaxLeafFormal.CDS.IsCDS G (X ∪ Y) @MaxLeafFormal.SteinerCDS.isState_JX : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (X : Finset V), MaxLeafFormal.SteinerCDS.IsState G (MaxLeafFormal.SteinerCDS.JX G X) @MaxLeafFormal.SteinerCDS.isState_Jb : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (J : MaxLeafFormal.SteinerCDS.State V) (b : V), MaxLeafFormal.SteinerCDS.IsState G (MaxLeafFormal.SteinerCDS.Jb G J b) @MaxLeafFormal.SteinerCDS.not_aSt_of_lt : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (X : Finset V), ∀ k < X.card, ¬MaxLeafFormal.SteinerCDS.aSt G X k @MaxLeafFormal.SteinerCDS.optSt_J0 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], G.Connected → (MaxLeafFormal.SteinerCDS.optSt G (MaxLeafFormal.SteinerCDS.JX G ∅) fun x => 1) = ↑(MaxLeafFormal.CDS.γc G) @MaxLeafFormal.SteinerCDS.optSt_eq_inf_Jb : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (J : MaxLeafFormal.SteinerCDS.State V), J.D = ∅ → ∀ (φ : V → ℕ), MaxLeafFormal.SteinerCDS.optSt G J φ = J.B.inf fun b => ↑(φ b) + MaxLeafFormal.SteinerCDS.optSt G (MaxLeafFormal.SteinerCDS.Jb G J b) φ @MaxLeafFormal.SteinerCDS.optSt_eq_optDir : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (J : MaxLeafFormal.SteinerCDS.State V), MaxLeafFormal.SteinerCDS.IsState G J → ∀ (φ : V → ℕ) (C₁ : Finset V) (h : C₁ ∈ J.D), MaxLeafFormal.SteinerCDS.optSt G J φ = MaxLeafFormal.SteinerDir.optDir (MaxLeafFormal.SteinerCDS.encAdj G J) (MaxLeafFormal.SteinerCDS.encWt J φ) (MaxLeafFormal.SteinerCDS.encRoot J C₁ h) (MaxLeafFormal.SteinerCDS.encTerm J C₁) @MaxLeafFormal.SteinerCDS.stateAlg_eq : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (J : MaxLeafFormal.SteinerCDS.State V), MaxLeafFormal.SteinerCDS.IsState G J → ∀ (φ : V → ℕ), MaxLeafFormal.SteinerCDS.stateAlg G J φ = MaxLeafFormal.SteinerCDS.optSt G J φ @MaxLeafFormal.SteinerCDS.terminals_JX : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (X : Finset V), (MaxLeafFormal.SteinerCDS.JX G X).R.card + (MaxLeafFormal.SteinerCDS.JX G X).D.card = MaxLeafFormal.CDS.termCount G X @MaxLeafFormal.SteinerDir.bIE_count : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] [inst_2 : DecidableRel A] (c : W → ℕ) (K : Finset W) (r : W) (L : ℕ), MaxLeafFormal.SteinerDir.bIE A c K r L = ↑{w | w.root = r ∧ MaxLeafFormal.SteinerDir.IsBW A w ∧ MaxLeafFormal.SteinerDir.blen (fun u => c u + 1) w = L ∧ K ⊆ w.labels}.ncard @MaxLeafFormal.SteinerDir.bw_count : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] [inst_2 : DecidableRel A] (c : W → ℕ) (Y : Finset W) (L : ℕ) (v : W), {w | w.root = v ∧ MaxLeafFormal.SteinerDir.IsBW A w ∧ MaxLeafFormal.SteinerDir.blen (fun u => c u + 1) w = L ∧ Disjoint w.labels Y}.Finite ∧ {w | w.root = v ∧ MaxLeafFormal.SteinerDir.IsBW A w ∧ MaxLeafFormal.SteinerDir.blen (fun u => c u + 1) w = L ∧ Disjoint w.labels Y}.ncard = MaxLeafFormal.SteinerDir.bw A c Y L v @MaxLeafFormal.SteinerDir.bw_mem : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] [inst_2 : DecidableRel A] (c : W → ℕ) (Y : Finset W) (L : ℕ), ∀ v ∈ Y, MaxLeafFormal.SteinerDir.bw A c Y L v = 0 @MaxLeafFormal.SteinerDir.bw_pos : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] [inst_2 : DecidableRel A] (c : W → ℕ) (Y : Finset W) (L : ℕ), ∀ v ∉ Y, 1 ≤ L → MaxLeafFormal.SteinerDir.bw A c Y L v = ∑ u with A v u ∧ u ∉ Y, ∑ L₁ ∈ Finset.range (L + 1 - (c u + 1)), MaxLeafFormal.SteinerDir.bw A c Y L₁ u * MaxLeafFormal.SteinerDir.bw A c Y (L - (c u + 1) - L₁) v @MaxLeafFormal.SteinerDir.bw_zero : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] [inst_2 : DecidableRel A] (c : W → ℕ) (Y : Finset W), ∀ v ∉ Y, MaxLeafFormal.SteinerDir.bw A c Y 0 v = 1 @MaxLeafFormal.SteinerDir.feasible_of_walk : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] (φ : W → ℕ) (r : W) (K : Finset W) (w : MaxLeafFormal.SteinerDir.BTree W), w.root = r → MaxLeafFormal.SteinerDir.IsBW A w → K ⊆ w.labels → MaxLeafFormal.SteinerDir.Feasible A r K (w.labels \ insert r K) ∧ Fintype.card W * ∑ v ∈ w.labels \ insert r K, φ v ≤ MaxLeafFormal.SteinerDir.blen (MaxLeafFormal.SteinerDir.arcLen φ r K) w @MaxLeafFormal.SteinerDir.steinerAlg_eq : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] [inst_2 : DecidableRel A] (φ : W → ℕ) (r : W) (K : Finset W), MaxLeafFormal.SteinerDir.steinerAlg A φ r K = MaxLeafFormal.SteinerDir.optDir A φ r K @MaxLeafFormal.SteinerDir.walk_of_feasible : ∀ {W : Type u_1} [inst : DecidableEq W] (A : W → W → Prop) [inst_1 : Fintype W] (φ : W → ℕ) (r : W) (K D : Finset W), MaxLeafFormal.SteinerDir.Feasible A r K D → ∃ w, w.root = r ∧ MaxLeafFormal.SteinerDir.IsBW A w ∧ K ⊆ w.labels ∧ MaxLeafFormal.SteinerDir.blen (MaxLeafFormal.SteinerDir.arcLen φ r K) w ≤ Fintype.card W * ∑ v ∈ D, φ v + (Fintype.card W - 1) @MaxLeafFormal.rstheta_tree_bound_0 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj], T.IsTree → ∀ (ν : V → ℕ), 6212 / 10000 * (747593601 / 960952792) ^ Fintype.card V * (512099210 / 652701491) ^ ∑ v, ν v ≤ MaxLeafFormal.treeW T ν (69 / 200) @MaxLeafFormal.rstheta_tree_bound_1 : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj], T.IsTree → ∀ (ν : V → ℕ), 6293 / 10000 * (248231700 / 312721579) ^ Fintype.card V * (568097827 / 739289481) ^ ∑ v, ν v ≤ MaxLeafFormal.treeW T ν (17 / 50) 'MaxLeafFormal.Antinorm3.PZ_add_Kcum' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.fin_nonneg_of_Kcum' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.init_all' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.merge_Kcum_left' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.merge_Kcum_right' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.merge_mem_smul_PZ' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.smul_PZ_add_Kcum' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.smul_PZ_mono' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.treeW_eq_fin' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.tree_bound_of_certificate' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.tree_bound_of_checks' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.triple_D_mem' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.triple_single' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Antinorm3.triple_split' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.budgeted_sound' depends on axioms: [propext, Quot.sound] 'MaxLeafFormal.Budget.budgeted_success' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.budgeted_success_of_admissible' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.cds_budgeted' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.cds_budgeted_maxLeaf' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.first_accepted' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.integral_twoPowNeg_pos' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.threshold_prob' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Budget.threshold_prob_upper' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.Zpart_iso' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.cc_gibbs' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.cc_path' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.cc_path_min' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.eIn_eq_induce' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.spr_eigen' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCGibbs.spr_facts' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCRate.cc_c3' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCRate.cc_cert' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCRate.spr_root' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCT.W_ge_Z' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCT.cc_T_a' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCT.cc_T_a_of_gibbs' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CCT.cc_T_a_of_hasCCBound' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.maxLeaf_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.maxLeaf_small' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.mean_terminals' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.moment_bound_of_tree_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.pointwise' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.rstheta_moment_bound_0' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.rstheta_moment_bound_1' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.spanningTree_of_CDS' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.tree_inequality' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.CDS.tree_reduction' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTCert.checkCert_sound' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTCert.dst_certs_exact' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTCert.dst_rates' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTCert.dst_rec' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTCert.dst_tree_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTCert.dst_tree_bound_WA' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTGraph.fa_dst_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTGraph.fa_dst_WS_minimum' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTGraph.fa_dst_point' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DSTGraph.fa_dst_point_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.DetRate.det_cert' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Lobster.M_mulVec' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Lobster.lobster_lower' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Lobster.lobster_upper' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.Lobster.u_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.Lam' depends on axioms: [propext, Quot.sound] 'MaxLeafFormal.LobsterGraph.Sstar' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.lobW_eq_matrix' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.lob_moments_lower' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.lob_moments_upper' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.mu_mul_pow_le_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.pow_le_choose_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.rst_caterpillar_c' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.rst_caterpillar_c_of_agree' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.LobsterGraph.tree_reduction_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.linear_savings_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.mls_budget' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.mls_sound' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.mls_success' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.mls_success_of_mean' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.mu_ge_of_mean' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.one_sample_size' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLS.star_of_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLSNec.Pnec' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLSNec.fw_gf_upper' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLSNec.mls_necessary' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLSNec.mu_mul_pow_le_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.MLSNec.pow_le_choose_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.Sstar_subset' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.card_eq_sum_pairs' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.exists_anchor' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.fa_pd_tight' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.matching_of_pairing' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pairing_of_matching' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_point' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_point_factor' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_rate_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_star' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_success' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_W_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_accepts' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_argmin' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_crit' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_min' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_moments' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_prob' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_ratio' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.pd_tight_unique' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDGraph.Ωpair_amgm' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDRate.pd_constants' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.PDRate.pd_rate' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCert.C5_of_stages' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCert.certificate_conditions' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCert.certificate_conditions_of' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCert.rsc_cone_a' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCert.rsc_cone_b' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCert.rsc_cone_c' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCompose.Wcl_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCompose.rsc_bound_trials' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCompose.rsc_maxLeaf_of_data' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCompose.rsc_rho_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCCompose.rsc_success_of_data' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.EQ2' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.EQ3' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.EQex' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.exists_ownerOK' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_bound_of_data' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_bound_of_data'' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_credit' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_credit_ex' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_jensen' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_jensen_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_jlemma' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_leaf' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_model' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_mono' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_pointwise' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_reduction' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCGraph.rsc_reduction_of' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCParams.rsc_C3' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCParams.rsc_lightpairs' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCParams.rsc_rsccredits' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCRec.rsc_messages' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTree.monotone_coupling' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTree.odds1' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTree.rsc_odds' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTree.rsc_recursion' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTree.rsc_recursion_fin' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTree.rsc_relaxed' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTrials.rsc_success_of_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTrials.rsc_trials_T2' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTrials.rsc_trials_T3' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSCTrials.rsc_trials_W' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRate.rsF_eq_Fstar' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRate.rsF_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRate.rs_constants' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRate.rs_rate_c' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rsTau_eq_τstar' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rs_base' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rs_base_denom' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rs_rate_a' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rs_rate_b' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rs_rate_b_argmin' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rsfσ_eq_fσ' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSRateAB.rsfσ_min_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaCert.cert0_Z' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaCert.cert0_inits' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaCert.cert0_pairs' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaCert.cert1_Z' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaCert.cert1_inits' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaCert.cert1_pairs' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaRate.rst_rates' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RSThetaRate.rst_rates_detail' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RateAssembly.rs_moments' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RateAssembly.rs_star' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.RateAssembly.rst_rate' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.aSt_iff_ext' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.aSt_iff_extYes' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.isSol_JX_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.isState_JX' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.isState_Jb' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.not_aSt_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.optSt_J0' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.optSt_eq_inf_Jb' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.optSt_eq_optDir' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.stateAlg_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerCDS.terminals_JX' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.bIE_count' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.bw_count' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.bw_mem' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.bw_pos' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.bw_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.feasible_of_walk' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.steinerAlg_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.SteinerDir.walk_of_feasible' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.rstheta_tree_bound_0' depends on axioms: [propext, Classical.choice, Quot.sound] 'MaxLeafFormal.rstheta_tree_bound_1' depends on axioms: [propext, Classical.choice, Quot.sound]