Skip to content

Adapt to math-comp/math-comp#1395 #68

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 2 commits into from
Apr 8, 2025
Merged

Adapt to math-comp/math-comp#1395 #68

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5578a68
Remove some %:R in favor of number notations
pi8027 Apr 7, 2025
f468be5
Adapt to math-comp/math-comp#1395
pi8027 Apr 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 14 additions & 10 deletions theories/BGappendixC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ have [_ /(mem_dprod defQ)[z [y [/setIP[_ cP0z] QP0y -> _]]]] := nU_P0Q.
by rewrite conjsgM (normsP (cent_sub P0)) //; exists y.
Qed.

Let E := [set x : galF | Nm x == 1 & Nm (2%:R - x) == 1].
Let E := [set x : galF | Nm x == 1 & Nm (2 - x) == 1].

Let E_1 : 1 \in E.
Proof. by rewrite !inE -addrA subrr addr0 galNorm1 eqxx. Qed.
Expand All @@ -246,7 +246,7 @@ Proof. by rewrite !inE -addrA subrr addr0 galNorm1 eqxx. Qed.
Let Einv_gt1_le_pq : E = [set x^-1 | x in E] -> (1 < #|E|)%N -> (p <= q)%N.
Proof.
rewrite (cardsD1 1) E_1 ltnS card_gt0 => Einv /set0Pn[/= a /setD1P[not_a1 Ea]].
pose tau (x : F) := (2%:R - x)^-1.
pose tau (x : F) := (2 - x)^-1.
have Etau x: x \in E -> tau x \in E.
rewrite inE => Ex; rewrite Einv (imset_f (fun y => y^-1)) //.
by rewrite inE andbC opprD addNKr opprK.
Expand Down Expand Up @@ -376,7 +376,7 @@ have [q_gt4 | q_le4] := ltnP 4 q.
by rewrite ltn_sub2l ?(ltn_exp2l 0) // prime_gt1.
rewrite -mulrDr -natrX -expnM muln2 -subn1 doubleB -addnn -addnBA // subn2.
rewrite expnD natrM -oP ler_wpM2l ?ler0n //.
apply: le_trans (_ : 2%:R * sqrtC #|P|%:R <= _).
apply: le_trans (_ : 2 * sqrtC #|P|%:R <= _).
rewrite mulrDl mul1r lerD2l -(@expr_ge1 _ 2) ?(ltW sqrtP_gt0) // sqrtCK.
by rewrite oP natrX expr_ge1 ?ler0n ?ler1n.
rewrite -ler_sqr ?rpredM ?rpred_nat ?qualifE ?(ltW sqrtP_gt0) //.
Expand All @@ -385,10 +385,14 @@ have [q_gt4 | q_le4] := ltnP 4 q.
by rewrite ?leq_exp2l // !doubleS !ltnS -addnn leq_addl.
have q3: q = 3%N by apply/eqP; rewrite eqn_leq qgt2 andbT -ltnS -(odd_ltn 5).
rewrite (cardsD1 1) E_1 ltnS card_gt0; apply/set0Pn => /=.
pose f (c : 'F_p) : {poly 'F_p} := 'X * ('X - 2%:R%:P) * ('X - c%:P) + ('X - 1).
have fc0 c: (f c).[0] = -1 by rewrite !hornerE /= !hornerE; apply/val_inj.
have fc2 c: (f c).[2%:R] = 1.
by rewrite !(subrr, hornerE) /= addrK; apply/val_inj.
pose f (c : 'F_p) : {poly 'F_p} := 'X * ('X - 2%:P) * ('X - c%:P) + ('X - 1).
(* TODO when requiring mathcomp >= 2.4.0, the following three lines
can be simplified to
have fc0 c: (f c).[0] = -1 by rewrite !hornerE.
have fc2 c: (f c).[2] = 1 by rewrite !(subrr, hornerE) /= addrK.
c.f. https://github.com/math-comp/odd-order/pull/68#discussion_r2030878922 *)
have fc0 c: (f c).[0] = -1 by rewrite !hornerE //= !hornerE.
have fc2 c: (f c).[2] = 1 by rewrite !(subrr, hornerE) /= addrK; apply/val_inj.
have /existsP[c nz_fc]: [exists c, ~~ [exists d, root (f c) d]].
have nz_f_0 c: ~~ root (f c) 0 by rewrite /root fc0 oppr_eq0.
rewrite -negb_forall; apply/negP=> /'forall_existsP/fin_all_exists[/= rf rfP].
Expand All @@ -400,7 +404,7 @@ have /existsP[c nz_fc]: [exists c, ~~ [exists d, root (f c) d]].
rewrite mulf_neq0 ?subr_eq0 1?(contraTneq _ (rfP a)) // => -> //.
by rewrite /root fc2.
have{nz_fc} /= nz_fc: ~~ root (f c) _ by apply/forallP; rewrite -negb_exists.
have sz_fc_lhs: size ('X * ('X - 2%:R%:P) * ('X - c%:P)) = 4%N.
have sz_fc_lhs: size ('X * ('X - 2%:P) * ('X - c%:P)) = 4%N.
by rewrite !(size_mul, =^~ size_poly_eq0) ?size_polyX ?size_XsubC.
have sz_fc: size (f c) = 4%N by rewrite size_addl ?size_XsubC sz_fc_lhs.
have irr_fc: irreducible_poly (f c) by apply: cubic_irreducible; rewrite ?sz_fc.
Expand Down Expand Up @@ -448,7 +452,7 @@ exists a; rewrite !inE; apply/and3P; split.
rewrite DfcF horner_prod -prodrN; apply: eq_bigr => beta _.
by rewrite rmorph0 hornerXsubC add0r opprK.
by rewrite -signr_odd mulr_sign oG horner_map fc0 rmorphN1 opprK.
apply/eqP; transitivity (fcF.[inF 2%:R]); last by rewrite horner_map fc2 rmorph1.
apply/eqP; transitivity (fcF.[inF 2]); last by rewrite horner_map fc2 rmorph1.
rewrite DfcF horner_prod; apply: eq_bigr => beta _.
by rewrite hornerXsubC rmorphB !rmorph_nat.
Qed.
Expand Down Expand Up @@ -615,7 +619,7 @@ suffices EpsiV a: a \in U -> psi a \in E -> psi (a^-1 ^ t ^+ 3) \in E.
rewrite -(odd_double_half #|P|) odd_P addnC.
elim: _./2 => [|n /EpsiV/EpsiV/=]; first by rewrite EpsiV -?Dx.
by rewrite conjVg invgK -!conjgM -!expgD -!mulnSr !(groupV, nUtn) //; apply.
move=> Ua Ea; have{Ea} [b Ub Dab]: exists2 b, b \in U & psi a + psi b = 2%:R.
move=> Ua Ea; have{Ea} [b Ub Dab]: exists2 b, b \in U & psi a + psi b = 2.
case/setIdP: Ea => _; rewrite -im_psi => /imsetP[b Ub Db]; exists b => //.
by rewrite -Db addrC subrK.
(* In the book k is arbitrary in Fp; however only k := 3 is used. *)
Expand Down
8 changes: 4 additions & 4 deletions theories/BGsection14.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1326,7 +1326,7 @@ Theorem Ptype_embedding M K :
{in Kstar^#, forall y, 'C_Mstar[y] = Z}
& {in K^# & Kstar^#, forall x y, 'C[x * y] = Z}]
& [/\ (*e*) [/\ normedTI Zhat G Z, {in ~: M, forall g, [disjoint Zhat & M :^ g]}
& (#|G|%:R / 2%:R < #|class_support Zhat G|%:R :> rat)%R ],
& (#|G|%:R / 2 < #|class_support Zhat G|%:R :> rat)%R ],
(*f*) M \in 'M_'P2 /\ prime #|K| \/ Mstar \in 'M_'P2 /\ prime #|Kstar|,
(*g*) {in 'M_'P, forall H, gval H \in M :^: G :|: Mstar :^: G}
& (*h*) M^`(1) ><| K = M]].
Expand Down Expand Up @@ -1768,7 +1768,7 @@ have hallKs: \sigma(M).-Hall(Mstar) Ks.
by rewrite subsetI sYMs (subset_trans sYMstar) ?gFnorm.
rewrite subsetI -{1}defKs_star subsetIl.
by rewrite (subset_trans (pHall_sub hallK)) ?gFnorm.
have oTGgt_g2: (g / 2%:R < #|TG|%:R)%R.
have oTGgt_g2: (g / 2 < #|TG|%:R)%R.
rewrite oTG big_setU1 //= /n defMNX big_set1 cards1 mulrC mul1r.
rewrite ltr_pM2r ?(ltr_nat _ 0) ?cardG_gt0 // /k_ K0 -defKs.
rewrite /z -defZ -(dprod_card defNK) natrM invfM opprD.
Expand Down Expand Up @@ -1867,15 +1867,15 @@ split=> // [||H PmaxH].
have [maxH _] := setDP PmaxH.
have{maxH}[L hallL] := Hall_exists \kappa(H) (mmax_sol maxH).
pose Ls := 'C_(H`_\sigma)(L); pose S := (L <*> Ls) :\: (L :|: Ls).
have{IHn} oSGgt_g2: (g / 2%:R < #|class_support S G|%:R)%R.
have{IHn} oSGgt_g2: (g / 2 < #|class_support S G|%:R)%R.
have [|nTG_leS] := ltnP #|class_support S G| nTG.
by case/IHn=> // Sstar _ [_ _ _ _ [[_ _ -> //]]].
apply: lt_le_trans oTGgt_g2 _; rewrite ler_nat /TG -defZhat.
exact: leq_trans leTGn nTG_leS.
have{oSGgt_g2 oTGgt_g2} meetST: ~~ [disjoint TG & class_support S G].
rewrite -leq_card_setU; apply: contraTneq (leqnn #|G|) => tiTGS.
rewrite -ltnNge -(ltr_nat rat) -/g.
rewrite -{1}[g](@divfK _ 2%:R) // mulr_natr.
rewrite -{1}[g](@divfK _ 2) // mulr_natr.
apply: lt_le_trans (ltrD oTGgt_g2 oSGgt_g2) _.
by rewrite -natrD -tiTGS ler_nat cardsT max_card.
have{meetST} [x Tx [a Sx]]: exists2 x, x \in T & exists a, x \in S :^ a.
Expand Down
5 changes: 2 additions & 3 deletions theories/PFsection1.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,8 +140,7 @@ by rewrite cfdotZl [d in _ * d]cfdotC Cmu rmorph0 mulr0.
Qed.

Let vchar_isometry_base3 f f' :
f \in 'Z[irr G, G^#] -> '[f]_G = 2%:R ->
f' \in 'Z[irr G, G^#] -> '[f']_G = 2%:R ->
f \in 'Z[irr G, G^#] -> '[f]_G = 2 -> f' \in 'Z[irr G, G^#] -> '[f']_G = 2 ->
'[f, f'] = 1 ->
exists es : _ * bool, let: (i, j, k, epsilon) := es in
[/\ f = (-1) ^+ epsilon *: ('chi_j - 'chi_i),
Expand Down Expand Up @@ -206,7 +205,7 @@ pose F i j := chi i - chi j.
have DF i j : F i j = F i 0 - F j 0 by rewrite /F opprB addrA subrK.
have ZF i j: F i j \in 'Z[Chi, L].
by rewrite zchar_split rpredB ?mem_zchar // DF memvB // /F !chiE.
have htau2 i j: i != j -> '[tau (F i j)] = 2%:R.
have htau2 i j: i != j -> '[tau (F i j)] = 2.
rewrite iso_tau // cfnormB -cfdotC !dot_chi !eqxx eq_sym => /negbTE->.
by rewrite -!natrD subr0.
have htau1 i j: j != 0 -> j != i -> i != 0 -> '[tau (F i 0), tau (F j 0)] = 1.
Expand Down
25 changes: 12 additions & 13 deletions theories/PFsection10.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,8 +312,7 @@ Local Notation Zalpha_tau := vchar_Dade_FTtype345_bridge.
(* This covers the last paragraph in the proof of (10.5); it's isolated here *)
(* because it is reused in the proof of (10.10) and (11.8). *)

Lemma norm_FTtype345_bridge i j :
j != 0 -> '[(alpha_ i j)^\tau] = 2%:R + n ^+ 2.
Lemma norm_FTtype345_bridge i j : j != 0 -> '[(alpha_ i j)^\tau] = 2 + n ^+ 2.
Proof.
move=> nz_j; rewrite Dade_isometry ?alpha_on // cfnormBd ?cfnormZ; last first.
by rewrite cfdotZr cfdotBl cfdotZl !o_mu2_zeta !(mulr0, subr0).
Expand All @@ -337,7 +336,7 @@ have [[_ Ddelta _ Nn] [[Itau1 Ztau1] _]] := (FTtype345_constants, cohS1).
have [|z Zz defY] := zchar_expansion _ S1_Y.
rewrite map_inj_in_uniq; first by case: sS10.
by apply: sub_in2 (Zisometry_inj Itau1); apply: mem_zchar.
have nX_2: '[X] = 2%:R.
have nX_2: '[X] = 2.
apply: (addrI '[Y]); rewrite -cfnormDd // addrC -Dalpha norm_alpha //.
by rewrite addrC nY_n2.
have Z_X: X \in 'Z[irr G].
Expand Down Expand Up @@ -417,7 +416,7 @@ have al_ij_zeta_s: '[al_ij^\tau, zeta^*^\tau1] = a.
have Zal_ij: al_ij^\tau \in 'Z[irr G] by apply: Zalpha_tau.
have Za: a \in Num.int.
by rewrite rpredD ?(intr_nat Nn) ?Cint_cfdot_vchar ?Ztau1 ?(mem_zchar Szeta).
have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R.
have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2 + n ^+ 2) * w1%:R.
have [k nz_k j'k]: exists2 k, k != 0 & k != j.
have:= w2gt2; rewrite -nirrW2 (cardD1 0) (cardD1 j) !inE nz_j !ltnS lt0n.
by case/pred0Pn=> k /and3P[]; exists k.
Expand All @@ -431,7 +430,7 @@ have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R.
rewrite !(cfdot_prTIirr_red pddM) cfdotC o_mu_zeta conjC0 !mulr0 mulr1.
by rewrite 2![_ == k](negPf _) 1?eq_sym // mulr0 -mulrN opprB !subr0 add0r.
have ZSmuk: mu_ k \in 'Z[calS] by rewrite mem_zchar ?calSmu.
have <-: '[al_ij^\tau] * '[(mu_ k)^\tau1] = (2%:R + n ^+ 2) * w1%:R.
have <-: '[al_ij^\tau] * '[(mu_ k)^\tau1] = (2 + n ^+ 2) * w1%:R.
by rewrite Itau1 // cfdot_prTIred eqxx mul1n norm_alpha.
by rewrite -intr_normK ?cfCauchySchwarz // Cint_cfdot_vchar // Ztau1.
suffices a0 : a = 0.
Expand Down Expand Up @@ -460,7 +459,7 @@ apply: le_lt_trans (_ : n ^+ 2 * (w1%:R - 1) < _).
rewrite -(ltr_pM2l (gt0CG W1)) -/w1 2!mulrBr mulr1 mulrCA -exprMn.
rewrite mulrDr ltrBlDl addrCA -mulrDr mulrCA mulrA -ltrBlDl.
rewrite -mulrBr mulNr opprK divfK ?neq0CG // mulr_natr addrA subrK -subr_sqr.
rewrite sqrr_sign mulrC [_ + 2%:R]addrC (lt_le_trans _ ub_da2) //.
rewrite sqrr_sign mulrC [_ + 2]addrC (lt_le_trans _ ub_da2) //.
apply: lt_le_trans (ler_wpM2l (ler0n _ _) a2_ge1).
by rewrite mulr1 ltrBlDl -mulrS -natrX ltC_nat.
Qed.
Expand Down Expand Up @@ -777,14 +776,14 @@ rewrite cards1 natrB ?addn_gt0 ?cardG_gt0 // addnC natrD -addrA mulrDl mulrBl.
rewrite {1}mulnC !natrM !invfM !mulVKf ?natrG_neq0 // opprD -addrA lerD2l.
rewrite mul1r -{1}[_^-1]mul1r addrC lerNr [- _]opprB -!mulrBl.
rewrite -addrA -opprD ler_pdivlMr; last by rewrite natrG_gt0.
apply: le_trans (_ : 1 - (3%:R^-1 + 7%:R^-1) <= _); last first.
apply: le_trans (_ : 1 - (3^-1 + 7^-1) <= _); last first.
rewrite lerD2l lerN2.
rewrite lerD // lef_pV2 ?qualifE/= ?gt0CG ?ltr0n ?ler_nat //.
have notStype5: FTtype S != 5%N by rewrite (eqP Stype2).
have frobUW2 := Ptype_compl_Frobenius maxS StypeP notStype5.
apply: leq_ltn_trans (ltn_odd_Frobenius_ker frobUW2 (mFT_odd _)).
by rewrite (leq_double 3).
apply: le_trans (_ : 2%:R^-1 <= _); last by rewrite -!CratrE; compute.
apply: le_trans (_ : 2^-1 <= _); last by rewrite -!CratrE; compute.
rewrite mulrAC ler_pdivrMr 1?gt0CG // ler_pdivlMl ?ltr0n //.
rewrite -!natrM ler_nat mulnA -(Lagrange (normal_sub nsM''M')) mulnC leq_mul //.
by rewrite subset_leq_card //; have [_ _ _ []] := MtypeP.
Expand Down Expand Up @@ -964,7 +963,7 @@ have [j nz_j] := has_nonprincipal_irr ntW2.
have [Dmu2_1 Ddelta_ lt1d Nn] := FTtype345_constants.
have{lt1d} [defS szS1 Dd Ddel Dn]:
[/\ perm_eq calS (S1 ++ S2), size S1 = (p ^ 2 - 1) %/ w1,
d = p, delta = -1 & n = 2%:R].
d = p, delta = -1 & n = 2].
- pose X_ (S0 : seq 'CF(M)) := [set s | 'Ind[M, H] 'chi_s \in S0].
pose sumX_ cS0 := \sum_(s in X_ cS0) 'chi_s 1%g ^+ 2.
have defX1: X_ S1 = Iirr_kerD H H H'.
Expand Down Expand Up @@ -1076,17 +1075,17 @@ have Dalpha i (al_ij := alpha_ i j) :
by rewrite Da_z' // intr_normK.
rewrite big_tnth sumr_const card_ord size_rem ?map_f // size_map.
by rewrite mulr_natl subn1.
have{lb_n2alij} ub_a2: (size S1)%:R * a ^+ 2 <= 2%:R * a * n + 2%:R.
have{lb_n2alij} ub_a2: (size S1)%:R * a ^+ 2 <= 2 * a * n + 2.
rewrite norm_alpha // addrC sqrrB !addrA lerD2r in lb_n2alij.
rewrite mulr_natl -mulrSr lerBlDl subn1 in lb_n2alij.
by rewrite -mulrA !mulr_natl; case: (S1) => // in S1zeta lb_n2alij *.
have{ub_a2} ub_8a2: 8%:R * a ^+ 2 <= 4%:R * a + 2%:R.
have{ub_a2} ub_8a2: 8 * a ^+ 2 <= 4 * a + 2.
rewrite mulrAC Dn -natrM in ub_a2; apply: le_trans ub_a2.
rewrite -intr_normK // ler_wpM2r ?exprn_ge0 ?normr_ge0 // leC_nat szS1.
rewrite (subn_sqr p 1) def_p_w1 subnK ?muln_gt0 // mulnA mulnK // mulnC.
by rewrite -subnDA -(mulnBr 2%N _ 1%N) mulnA (@leq_pmul2l 4 2) ?ltn_subRL.
have Z_4a1: 4%:R * a - 1%:R \in Num.int by rewrite rpredB ?rpredM ?rpred_nat.
have{ub_8a2} ub_4a1: `|4%:R * a - 1| < 3%:R.
have Z_4a1: 4 * a - 1 \in Num.int by rewrite rpredB ?rpredM ?rpred_nat/=.
have{ub_8a2} ub_4a1: `|4 * a - 1| < 3.
rewrite -ltr_sqr ?rpred_nat ?qualifE/= ?normr_ge0 // -natrX intr_normK //.
rewrite sqrrB1 exprMn -natrX -mulrnAl -mulrnA (natrD _ 8 1) ltrD2r.
rewrite (natrM _ 2 4) (natrM _ 2 8) -!mulrA -mulrBr ltr_pM2l ?ltr0n //.
Expand Down
8 changes: 4 additions & 4 deletions theories/PFsection11.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ Lemma bounded_proper_coherent H1 :
(#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
Proof.
move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU.
suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
suffices: #|HU : H1|%:R - 1 <= 2 * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -lerBlDr -mulnA natrM.
congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)).
rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC.
Expand Down Expand Up @@ -884,18 +884,18 @@ have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
rewrite cfRes_cfun1 !cfdotBl deltaZ !cfdotZl -!/(mu2_ 0 _).
rewrite -(prTIirr00 ptiWM) !cfdot_prTIirr cfdotC omu2S1 // conjC0 mulr0.
by rewrite (negPf nz_j1) add0r subr0 subrr rpred0.
have nY: '[Y] = n * a * (a - 2%:R) + n ^+ 2. (* Resuming step (11.8.2). *)
have nY: '[Y] = n * a * (a - 2) + n ^+ 2. (* Resuming step (11.8.2). *)
rewrite defY cfnormD cfnormN !cfnormZ cfdotNr cfdotZr.
rewrite cfnorm_map_orthonormal // -Dn Itau1 ?mem_zchar ?n1S1 // mulr1.
rewrite scaler_sumr cfproj_sum_orthonormal // rmorphN addrAC.
rewrite Dn rmorphM/= !intr_normK ?rpred_nat // !rmorph_nat conj_intr // -Dn.
by rewrite -mulr2n mulrC mulrA -[in LHS]mulr_natr mulNr -mulrBr.
have{a_even} Da: (a == 0) || (a == 2%:R). (* Second part of (11.8.2). *)
have{a_even} Da: (a == 0) || (a == 2). (* Second part of (11.8.2). *)
suffices (b := a - 1): b ^+ 2 == 1.
by rewrite -!(can_eq (subrK 1) a) add0r addrK orbC -eqf_sqr expr1n.
have S1gt0: (0 < size S1)%N by case: (S1) S1zeta.
have: n * b ^+ 2 <= n *+ 3.
have: 2%:R + n <= n *+ 3 by rewrite addrC lerD2l lerMn2r Dn ler1n.
have: 2 + n <= n *+ 3 by rewrite addrC lerD2l lerMn2r Dn ler1n.
apply: le_trans; rewrite sqrrB1 -(mulr_natr a) -mulrBr mulrDr mulrA mulr1.
rewrite lerD2r -(lerD2r (n ^+ 2 + '[X])) !addrA -nY -cfnormDd //.
by rewrite -Dphi norm_FTtype345_bridge ?S1_1 // lerDl cfnorm_ge0.
Expand Down
12 changes: 6 additions & 6 deletions theories/PFsection12.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -982,7 +982,7 @@ have norm_alpha: '[tauL_H alpha] = e%:R + 1.
rewrite Dade_isometry ?(cfInd1_sub_lin_on _ Schi) ?De //.
rewrite cfnormBd; last by rewrite cfdotC (seqInd_ortho_Ind1 _ _ Schi) ?conjC0.
by rewrite cfnorm_Ind_cfun1 // De irrWnorm.
pose h := #|H|; have ub_a: a ^+ 2 * ((h%:R - 1) / e%:R) - 2%:R * a <= e%:R - 1.
pose h := #|H|; have ub_a: a ^+ 2 * ((h%:R - 1) / e%:R) - 2 * a <= e%:R - 1.
rewrite -[h%:R - 1](mulKf (neq0CiG L H)) -sum_seqIndC1_square // De -/calS.
rewrite -[lhs in lhs - 1](addrK 1) -norm_alpha -[tauL_H _](subrK 1).
rewrite cfnormDd; last by rewrite cfdotBl tau_alpha_1 cfnorm1 subrr.
Expand All @@ -1002,7 +1002,7 @@ have [pr_p p_dv_M]: prime p /\ p %| #|M|.
by rewrite mem_primes => /and3P[].
have odd_p: odd p by rewrite (dvdn_odd p_dv_M) ?mFT_odd.
have pgt2: (2 < p)%N := odd_prime_gt2 odd_p pr_p.
have ub_e: e%:R <= (p%:R + 1) / 2%:R :> algC.
have ub_e: e%:R <= (p%:R + 1) / 2 :> algC.
rewrite ler_pdivlMr ?ltr0n // -natrM -mulrSr leC_nat muln2.
have [b e_dv_pb]: exists b : bool, e %| (b.*2 + p).-1.
by have [_ /orP[]] := Ecyclic_le_p; [exists false | exists true].
Expand All @@ -1013,7 +1013,7 @@ have ub_e: e%:R <= (p%:R + 1) / 2%:R :> algC.
have lb_h: p%:R ^+ 2 <= h%:R :> algC.
rewrite -natrX leC_nat dvdn_leq ?pfactor_dvdn ?cardG_gt0 //.
by rewrite -prankP0 (leq_trans (p_rankS p sP0H)) ?p_rank_le_logn.
have{ub_e} ub_a: p.-1.*2%:R * a ^+ 2 - 2%:R * a <= p.-1%:R / 2%:R :> algC.
have{ub_e} ub_a: p.-1.*2%:R * a ^+ 2 - 2 * a <= p.-1%:R / 2 :> algC.
apply: le_trans (le_trans ub_a _); last first.
rewrite -subn1 -subSS natrB ?ltnS ?prime_gt0 // mulrSr mulrBl.
by rewrite divff ?pnatr_eq0 ?lerD2r.
Expand All @@ -1026,11 +1026,11 @@ have a0: a = 0.
apply: contraTeq ub_a => nz_a; rewrite lt_geF // ltr_pdivrMr ?ltr0n //.
rewrite mulrC -{1}mulr_natl -muln2 natrM -mulrA mulrBr mulrCA ltrBrDl.
rewrite -ltrBrDr -mulrBr mulr_natl mulrA -expr2 -exprMn.
apply: lt_le_trans (_ : 2%:R * ((a *+ 2) ^+ 2 - 1) <= _); last first.
apply: lt_le_trans (_ : 2 * ((a *+ 2) ^+ 2 - 1) <= _); last first.
rewrite (mulr_natl a 2) ler_wpM2r // ?subr_ge0.
by rewrite sqr_intr_ge1 ?rpredMn // mulrn_eq0.
by rewrite leC_nat -subn1 ltn_subRL.
rewrite -(@ltr_pM2l _ 2%:R) ?ltr0n // !mulrA -expr2 mulrBr -exprMn mulr1.
rewrite -(@ltr_pM2l _ 2) ?ltr0n // !mulrA -expr2 mulrBr -exprMn mulr1.
rewrite -natrX 2!mulrnAr -[in rhs in _ < rhs]mulrnAl -mulrnA.
rewrite ltrBrDl -ltrBrDr -(ltrD2r 1) -mulrSr -sqrrB1.
rewrite -intr_normK ?rpredB ?rpredM ?rpred_nat ?rpred1 //.
Expand Down Expand Up @@ -1228,7 +1228,7 @@ have{lb_psiM lb_psiL ub_rhoML ubM} ubK: (#|K / K'|%g < 4)%N.
rewrite ler_pdivrMr ?gt0CG // ler_pdivlMl ?gt0CG //.
by rewrite ler_pdivrMr ?gt0CG // mulrC -natrM leC_nat.
rewrite -(ler_pM2l (gt0CG E)) -/e mulrA -expr2 invfM -exprMn.
apply: le_trans (_ : (1 + 2%:R^-1) ^+ 2 <= _).
apply: le_trans (_ : (1 + 2^-1) ^+ 2 <= _).
rewrite ler_sqr ?rpred_div ?rpredD ?rpred1 ?rpredV ?rpred_nat //.
rewrite -{1}(ltn_predK egt2) mulrSr mulrDl divff ?gt_eqF // lerD2l.
rewrite ler_pdivrMr // ler_pdivlMl ?ltr0n //.
Expand Down
Loading
Loading