proposition: Lemma tree_like_after (lam rho : NormalizedDegreeDistribution.L K) c r len l : partial_connected c -> tree_like c -> (size lam <= maxdeg)%nat -> (size rho <= maxdeg)%nat -> (#|ports (nodes c)| <= len)%nat -> (#|known_coports c| <= len)%nat -> border (conodes c) = set0 -> r > 0 -> (len * tree_max l.+1 < #|port|)%nat -> let next_graphs := build_graphs lam rho c r l in (weighted_count (@tree_like _) next_graphs / weighted_count predT next_graphs) >= ((#|port| - len * tree_max l.+1)%:R / #|port|%:R) ^+ (len * tree_max l).
proof: Proof. elim: l lam rho len c r => [|l IHl] /= lam rho len c r Hpc Htl Hlam Hrho Hlen Hclen Hcob Hr Hlenmax. subst build_graphs => /=. rewrite dest_ports_seqs_0 /=. rewrite /image_mem enum_set1 /=. rewrite /weighted_count !big_cons !big_nil /= Htl. rewrite addr0 divrr ?unitf_gt0 //. by rewrite /tree_max big_ord0 muln0 expr0. have Hlenmax' := Hlenmax. rewrite /tree_max sum_expr_S mulnDr muln1 mulnA in Hlenmax. rewrite [tree_max l.+1]sum_expr_S mulnDr muln1 mulnA. rewrite [tree_max l.+2]sum_expr_S mulnDr muln1 mulnA. set len' := (len * maxdeg.+1)%nat in Hlenmax *. rewrite exprD. set r1 := _ ^+ len. set r2 := _ ^+ _. have Hb: (#|border (nodes c)| <= len)%nat. by rewrite (leq_trans (card_border_ports _)). have Hr1: r1 > 0. apply exprn_gt0, divr_gt0. by rewrite ltr0n ltn_subRL addn0. by rewrite ltr0n; apply/card_gt0P; exists def_port. have Hr2: r2 > 0. apply exprn_gt0, divr_gt0. by rewrite ltr0n ltn_subRL addn0. by rewrite ltr0n; apply/card_gt0P; exists def_port. rewrite 2!weighted_count_switch_step le_sum_all_cond //; try by move=> ? _; apply weighted_count_switch_ge0. rewrite -weighted_count_switch_step. by rewrite (weighted_count_switch_it r Hlam Hrho Hlen). rewrite [X in _ <= X](bigID(fun i : _ .-tuple _ => tree_like (step_it c i))) /=. apply: ler_wpDr; first by apply: sumr_ge0 => i _; exact: weighted_count_switch_ge0. set F := BIG_F. apply (@Order.POrderTheory.le_trans _ _ (\sum_(i in dest_ports c #|border (nodes c)| | tree_like (step_it c i)) F i)). rewrite (bigID xpredT) /= [in X in _ + X]big_pred0 ?addr0; last first. by move=> ?; rewrite andbF. have HF: forall P, \sum_(i in dest_ports c #|border (nodes c)| | P i) F i = \sum_(i in dest_ports c #|border (nodes c)| | P i) (step_dist_it lam c r i).2. move=> P; apply eq_bigr => i /andP [Hi _]; rewrite /F. rewrite tuple_to_partial_enumK. rewrite (surjective_pairing (step_dist_it _ _ _ _)) /=. case/boolP: ((step_dist_it lam c r i).2 == 0) => Hi2. rewrite (eqP Hi2). rewrite /weighted_count big_map /= big1 //. move=> ? _; rewrite switch_step_dist_it_const. by destruct switch_step_dist_it; rewrite mul0r. move: (@weighted_count_switch_it len' rho lam (switch (step_it c i)) (step_dist_it lam c r i).2). rewrite /build_graphs. rewrite -(step_dist_it_1 lam c r). apply => //. by rewrite step_dist_it_1 (ports_conodes_step_it Hi Hi2). rewrite step_dist_it_1 /known_coports /ports part_nodes_step_it. apply (leq_trans Hlen). by rewrite /len' mulnS leq_addr. by rewrite step_dist_it_1 border_nodes_step_it. by rewrite (leq_ltn_trans _ Hlenmax) // leq_addl. rewrite 2!{}HF {F}. have Hb': (#|border (nodes c)| * maxdeg < #|port| - #|known_coports c|)%nat. apply (@leq_ltn_trans (#|ports (nodes c)| * maxdeg)). apply leq_mul => //. by apply card_border_ports. rewrite ltn_subRL. apply (@leq_ltn_trans (len * maxdeg.+1)). by rewrite mulnS leq_add // leq_mul. rewrite (leq_ltn_trans _ Hlenmax) //. by rewrite sum_expr_S mulnDr addnA (addnC len) -addnA muln1 leq_addr. rewrite big_mkcondr /= -ler_pdivlMr; last first. move: (weighted_count_it Hlam def_port r (leqnn _) Hb'). by rewrite /weighted_count big_map big_enum_in => ->. move: (tree_like_empty_border Hlam def_port Hpc Htl Hr Hb') => /=. rewrite /weighted_count 2!big_map big_enum_in /=. rewrite big_mkcond big_enum_in -big_mkcondr /=. set r0 := _ / _. set tl1 := \sum_(i in _ | tree_like _) _. set tl2 := \sum_(i in _ | tree_like _) _. have -> : tl1 = tl2. apply eq_bigl => /= i. by rewrite step_dist_it_1. have Hfree: (#|free_coports c| > 0)%nat. rewrite cardsCs setCK cardsD ltn_subRL addn0. apply (leq_ltn_trans (leq_subr _ _)). apply (leq_ltn_trans Hclen). by rewrite (leq_ltn_trans _ Hlenmax) // leq_addr. apply Order.POrderTheory.le_trans. apply (@Order.POrderTheory.le_trans _ K (r0 ^+ len)). rewrite /r1. apply: lerXn2r. by rewrite rpred_div // nnegrE ler0n. by rewrite rpred_div // nnegrE ler0n. apply: ler_pM. exact: ler0n. by rewrite invr_ge0 ler0n. rewrite ler_nat. rewrite -subnDA leq_sub2l //. apply leq_add => //. rewrite sum_expr_S mulnDr muln1. apply (@leq_trans len'). by rewrite mulnC leq_mul. by rewrite leq_addr. rewrite ler_pV2 //. by rewrite ler_nat max_card. by rewrite inE unitf_gt0 // ltr0n /=; apply/card_gt0P; exists def_port. by rewrite inE unitf_gt0 // ltr0n. rewrite -(subnK Hb) exprD. rewrite ger_pMl //. apply: exprn_ile1. by rewrite mulr_ge0 ?ler0n // invr_ge0 ler0n. rewrite ler_pdivrMr ?mul1r. rewrite ler_nat (cardsCs (free_coports _)) setCK -subnDA. apply/leq_sub2l/(@leq_trans #|known_coports c|). by rewrite cardsD leq_subr. by rewrite leq_addr. by rewrite ltr0n. apply/exprn_gt0/mulr_gt0. by rewrite ltr0n ltn_subRL addn0 mulnC. by rewrite invr_gt0 ltr0n. rewrite {}/F le_eqVlt. apply /orP /or_introl /eqP. rewrite (bigID (fun i : _ .-tuple _ => (step_dist_it lam c r i).2 == 0)) big1 ?add0r; last first. move=> i /andP [] /andP [Hi _] Hd. rewrite tuple_to_partial_enumK. rewrite (surjective_pairing (step_dist_it _ _ _ _)) /=. rewrite (eqP Hd). rewrite /weighted_count big_map /= big1 //. move=> j _; rewrite switch_step_dist_it_const. by destruct switch_step_dist_it; rewrite mul0r. rewrite [in RHS](bigID (fun i : _ .-tuple _ =>(step_dist_it lam c r i).2 == 0)) [in RHS]big1 /= ?add0r; last first. move=> i /andP [] /andP [Hi _] Hd. rewrite tuple_to_partial_enumK. rewrite (surjective_pairing (step_dist_it _ _ _ _)) /=. rewrite (eqP Hd). rewrite /weighted_count big_map /= big1 //. move=> j _; rewrite switch_step_dist_it_const. by destruct switch_step_dist_it; rewrite mul0r. apply eq_bigl => i. apply andb_id2r => Hd; rewrite -andbA; apply andb_id2l => Hi. case/boolP : (tree_like _) => Htli; last by rewrite andbF. symmetry; rewrite andbT. rewrite tuple_to_partial_enumK. rewrite (surjective_pairing (step_dist_it _ _ _ _)) step_dist_it_1 /=. have Hpci: partial_connected (switch (step_it c i)). destruct i as [i ?] => /=. clear -Hpc. apply connected_switch. rewrite /step_it. elim: i c (enum _) Hpc => /= [|x i IH] c [|s b] Hpc //=. by apply IH, connected_step. move/(_ rho lam len' _ (step_dist_it lam c r i).2 Hpci): IHl. rewrite tree_like_switch. move/(_ Htli Hrho Hlam). move/(_ (ports_conodes_step_it Hi Hd Hlam Hlen Hclen)). have Hlen': (#|known_coports (switch (step_it c i))| <= len')%nat. rewrite /known_coports /ports part_nodes_step_it. by rewrite /len' mulnS (leq_trans Hlen) // leq_addr. have Hd': (step_dist_it lam c r i).2 > 0. by rewrite lt_def Hd step_dist_it_ge0 // ltW. have Hlenmaxrec: (len' * tree_max l.+1 < #|port|)%nat. by rewrite (leq_ltn_trans _ Hlenmax) // leq_addl. move/(_ Hlen' (border_nodes_step_it Hi) Hd' Hlenmaxrec) => /=. apply Order.POrderTheory.le_trans. apply: lerXn2r. by rewrite rpred_div // nnegrE ler0n. by rewrite rpred_div // nnegrE ler0n. rewrite ler_pM ?ler0n//. by rewrite invr_ge0 ler0n. by rewrite subnDA subnAC ler_nat leq_subr. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner