proposition: Lemma tree_like_empty_border c r : partial_connected c -> tree_like c -> r > 0 -> let len := #| border (nodes c) | in (len * maxdeg < #|port| - #|known_coports c|)%nat -> let next_graphs := [seq step_dist_it c r (tval dests) | dests in dest_ports c len] in (weighted_count (@tree_like _) next_graphs / weighted_count predT next_graphs) >= ((#|port| - #|known_coports c| - maxdeg * len)%:R / #|free_coports c|%:R) ^+ len.
proof: Proof. move eqk : #|border (nodes c)| => k. elim: k c r eqk => [|k IHk] /= c r eqk Hpc Htl Hr Hlam. rewrite expr0. move/eqP: eqk. rewrite cards_eq0 => /eqP eqk. rewrite /step_dist_it. rewrite eqk /= enum_set0 /=. rewrite dest_ports_0. rewrite /image_mem enum_set1 /=. rewrite /weighted_count !big_cons !big_nil /= Htl. by rewrite addr0 divrr // unitf_gt0. rewrite !weighted_count_step; try by rewrite eqk. move: (eqk). rewrite cardE. move eqb : (enum (border (nodes c))) => [//|s b] _. have Hhead: head def_port (s :: b) \in border (nodes c). by rewrite -mem_enum eqb inE eqxx. have Hlam': (maxdeg <= #|port| - #|known_coports c|)%nat. rewrite mulSn /= in Hlam. by apply (leq_trans (leq_addr _ _) (ltnW Hlam)). rewrite exprS. set r1 := _ / _. set r2 := _ ^+ k. have Hknownp: (#|port| - #|known_coports c| > 0)%nat. by rewrite (leq_trans _ (leq_trans Hmax Hlam')) // lt0n DegreeDistribution.psize. have Hfreep: (#|free_coports c| > 0)%nat. rewrite /free_coports cardsCs setCK cardsD. rewrite subn_gt0 in Hknownp. by rewrite subn_gt0 (leq_ltn_trans _ Hknownp) // leq_subr. have Hknownp': (#|port| - #|known_coports c| - maxdeg * k.+1 > 0)%nat. by rewrite ltn_subRL addn0 mulnC. have Hr1: r1 > 0 by rewrite divr_gt0 // ltr0n. have Hr2: r2 > 0 by apply exprn_gt0. apply (le_sum_all_cond Hr1 Hr2); try by move=> ? _; apply weighted_count_it_ge0. by rewrite -(weighted_count_step r _) ?eqk // weighted_count_it // -eqk. rewrite [X in _ <= X](bigID (fun i : port * {set port} => i.2 \notin conodes c)) /=. apply: ler_wpDr; first by apply: sumr_ge0 => i _; exact: weighted_count_it_ge0. set F := BIG_F. apply (@Order.POrderTheory.le_trans _ _ (\sum_(i in dest_port c | tree_like (step c (bnext c) i.1 i.2)) F i)). rewrite (bigID xpredT) /= [in X in _ + X]big_pred0 ?addr0; last first. by move=> ?; rewrite andbF. do 2 (rewrite (sum_weighted_count_it r _ eqb) // ?eqk //; last by move=> ? ?; apply weighted_count_it). rewrite (eq_bigl (mem (dest_port c))); last by move=> ?; rewrite andbT. rewrite -big_distrl -big_distrr /= mulrC -ler_pdivlMl; last first. move: (weight_is_dist Hhead (leq_trans Hmax Hlam')). rewrite /weighted_count big_map big_enum_in -big_distrl /=. by rewrite -big_distrr /= mul1r -mulrA => ->; by rewrite mulr1. rewrite mulrC -big_distrl -big_distrr /=. move: (tree_like_step Htl Hhead (leq_trans Hmax Hlam') Hpc). rewrite /weighted_count 2!big_map big_enum_in -2!big_distrl /=. rewrite -2!big_distrr /= 2!mul1r big_mkcond big_enum_in -big_mkcondr /=. rewrite -3!mulf_div (@mulfV _ r) ?gt_eqF // mulfV; last first. by rewrite invr_neq0 // pnatr_eq0 -lt0n. rewrite mul1r /bnext eqb /= => ->. by rewrite ler_pM // ?ler_nat ?leq_subr // ?invr_ge0 ltW // ltr0n. rewrite {}/F le_eqVlt. apply /orP /or_introl /eqP. rewrite (bigID (fun i => dest_dist c i.2 == 0)) /= big1; last first. by move=> i /andP[_]; apply weighted_count_it_eq0; rewrite eqb. rewrite add0r [in RHS](bigID (fun i => dest_dist c i.2 == 0)) /=. rewrite [in RHS]big1 ?add0r; last first. by move=> i /andP[_]; apply weighted_count_it_eq0; rewrite eqb. apply eq_bigl => i. apply andb_id2r => Hd; rewrite -andbA; apply andb_id2l => Hi. move/andP: (step_dest_port Hhead Hi) => [Htriv Hcond]. case/boolP : (i.2 \in _) => Hni; rewrite (andbF, andbT). rewrite /bnext eqb; apply/negP. move/(tree_like_no_sharing Hhead Hpc Htriv Hcond)/negP; apply. apply/bigcupP; exists i.2 => //. by move: Hi; rewrite inE => /and3P[]. have Htl' : tree_like (step c (bnext c) i.1 i.2). rewrite /bnext eqb; apply no_sharing_tree_like => //. apply/negP => Hi1. move/andP: Hcond => [_]. rewrite /step_end_cond inE => /andP [_ Hi2]. by rewrite (trivIset_I1 Htriv Hi2) in Hni. rewrite Htl'; symmetry. move: (eqk). rewrite cardE eqb -(enum_step_border eqb Hi) => /= [] []. rewrite -cardE => Hk. move: Htl' (IHk (step c (bnext c) i.1 i.2) (r * dest_dist c i.2 / #|free_coports c|%:R)) => /=. rewrite /bnext eqb /= => Htl'. set r' := r * _ / _. have Hrd: r' > 0. by rewrite divr_gt0 // ?ltr0n // mulr_gt0 // lt0r Hd dest_dist_ge0. move: (free_step_coports_gt Hlam Hhead Hi Hd) => Hlam1. move/(_ Hk (connected_step Hpc) Htl' Hrd Hlam1). rewrite /weighted_count /step_dist_it eqb /= /(step_dist c r s i). rewrite (enum_step_border eqb Hi) -/r'. apply Order.POrderTheory.le_trans. rewrite /r2 /r1. apply: lerXn2r. by rewrite nnegrE ltW. by rewrite nnegrE divr_ge0 // ler0n. rewrite ler_pM // ?invr_ge0 ?ler0n //. rewrite ler_nat mulnS subnDA leq_sub2r // -subnDA leq_sub2l //. rewrite /known_coports step_coports_ok //. rewrite cardsU addnC leq_subLR addnCA leq_add2l. by rewrite (leq_trans (cards_conode_out Hd Hni)) // leq_addl. have Hfc : (#|free_coports (step c s i.1 i.2)| > 0)%nat. rewrite (@leq_ltn_trans (k * maxdeg)%nat) // (leq_trans Hlam1)//. rewrite (cardsCs (~: _)) setCK. by rewrite leq_sub2l // cardsD /= leq_subr. rewrite lef_pV2 // ?posrE ?ltr0n //. rewrite (cardsCs (~: _)) setCK (cardsCs (~: _)) setCK. rewrite ler_nat leq_sub2l // step_codom_ok //. exact/subset_leq_card/subsetUr. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner