Skip to content

style: resolve linter warnings and format long lines #369

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

Open
sqrt-of-2 wants to merge 1 commit into
base: main
Choose a base branch
from
Open

style: resolve linter warnings and format long lines #369

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
6 changes: 3 additions & 3 deletions RealRooted/BorceaBranden/FiniteSymbolReciprocal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ private theorem rightComplementMonomial_one
(sumInrEmbedding tau sigma) (Finset.univ \ m.1.support)

private theorem degreeOf_rightComplementMonomial_one_le
{sigma tau : Type*} [Fintype sigma] [DecidableEq sigma]
{sigma tau : Type*} [Fintype sigma]
(m : {m : sigma →₀ ℕ // ∀ i, m i ≤ 1}) :
∀ i : sigma,
(rightComplementMonomial (R := ℂ) (τ := tau)
Expand All @@ -123,7 +123,7 @@ private theorem degreeOf_rename_inl_le_zero
by_contra hdi
have hmem : Sum.inr i ∈
(rename (Sum.inl : tau → Sum tau sigma) A).vars := by
rw [mem_vars]
rw [mem_vars_iff_mem_support]
exact ⟨d, hd, Finsupp.mem_support_iff.mpr hdi⟩
obtain ⟨j, hj, hji⟩ := mem_vars_rename Sum.inl A hmem
exact Sum.inl_ne_inr hji
Expand Down Expand Up @@ -174,7 +174,7 @@ private theorem signedMultiaffineReciprocalRight_target_mul
ring

private theorem normalized_reciprocal_rightComplementMonomial_one
{sigma tau : Type*} [Fintype sigma] [DecidableEq sigma]
{sigma tau : Type*} [Fintype sigma]
(m : {m : sigma →₀ ℕ // ∀ i, m i ≤ 1}) :
C ((-1 : ℂ) ^ Fintype.card sigma) *
signedMultiaffineReciprocalRight
Expand Down
3 changes: 2 additions & 1 deletion RealRooted/PosCombo.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -739,7 +739,8 @@ theorem of_aissenSchoenbergWhitney_right_pencil
C a * (f + C z * g) = C a * f + C b * g := by
grind
rw [← hscale]
exact ⟨mul_ne_zero (by grind) (hne hz), .mul (.C _) <| (aissenSchoenbergWhitneyForward (hpf hz)).1⟩
exact ⟨mul_ne_zero (by grind) (hne hz),
.mul (.C _) <| (aissenSchoenbergWhitneyForward (hpf hz)).1⟩

/--
TNN-named version of `of_aissenSchoenbergWhitney_right_pencil`.
Expand Down
3 changes: 1 addition & 2 deletions RealRooted/SameDegreeCubicSecondRootFromAnalytic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,7 @@ private theorem card_filter_lt_triple (a b c x : ℝ) :
Chudnovsky--Seymour root-count theorem. -/
theorem cubicSecondRootBound_from_analytic : CubicSecondRootBoundStatement := by
classical
intro f g hf_pos hg_pos hf hg hfdeg hgdeg hpc
intro a b c p q r hab hbc hpq hqr hfroots hgroots
intro f g hf_pos hg_pos hf hg hfdeg hgdeg hpc a b c p q r hab hbc hpq hqr hfroots hgroots
have hdeg : g.natDegree = f.natDegree := by
simp [hfdeg, hgdeg]
by_cases hno : ∀ z, f.IsRoot z → ¬ g.IsRoot z
Expand Down
9 changes: 6 additions & 3 deletions RealRooted/Tactic/VeroneseSection.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,8 @@ theorem veroneseSectionPolynomial_sequence_zero_or_splits_of_nonneg
∀ n : Nat,
veroneseSectionPolynomial (r n) (k n) (P n) = 0 ∨
(veroneseSectionPolynomial (r n) (k n) (P n)).Splits := fun n =>
veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg (hnn n) (hsplits n) (hr n) (hk n)
veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg
(hnn n) (hsplits n) (hr n) (hk n)

theorem prec0_veroneseSectionPolynomial_sequence_of_prec
{r k : Nat → Nat} {P Q : Nat → ℝ[X]}
Expand Down Expand Up @@ -337,7 +338,8 @@ macro_rules
k_lt_r := $hk:term) =>
`(tactic|
exact
RealRooted.veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg $hpnn $hsplits $hr $hk)
RealRooted.veroneseSectionPolynomial_eq_zero_or_isRealRooted_of_realRooted_nonneg
$hpnn $hsplits $hr $hk)
| `(tactic|
rr_veronese_section_prec0 using
prec_to_full := $hPrecToFull:term,
Expand Down Expand Up @@ -434,7 +436,8 @@ macro_rules
k_lt_r := $hk:term) =>
`(tactic|
exact
RealRooted.veroneseSectionPolynomial_sequence_zero_or_splits_of_nonneg $hpnn $hsplits $hr $hk)
RealRooted.veroneseSectionPolynomial_sequence_zero_or_splits_of_nonneg
$hpnn $hsplits $hr $hk)
| `(tactic|
rr_veronese_section_sequence_prec0 using
prec_to_full := $hPrecToFull:term,
Expand Down
6 changes: 4 additions & 2 deletions RealRooted/VeroneseSection.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1659,7 +1659,8 @@ theorem splits_veroneseSectionPolynomial_of_pf {p : ℝ[X]}
veroneseSectionPolynomial r k p = 0 ∨
(veroneseSectionPolynomial r k p).Splits :=
Or.inr
(aissenSchoenbergWhitneyForward (IsPolyaFreqSeq_veroneseSectionPolynomial_coeff (p := p) hp hr hk)).1
(aissenSchoenbergWhitneyForward
(IsPolyaFreqSeq_veroneseSectionPolynomial_coeff (p := p) hp hr hk)).1

/-- Zero-aware real-rootedness of Veronese sections from the forward ASW
theorem and a PF certificate for the original polynomial. -/
Expand Down Expand Up @@ -1689,7 +1690,8 @@ theorem splits_veroneseSectionPolynomial_of_splits_nonneg {p : ℝ[X]}
veroneseSectionPolynomial r k p = 0 ∨
(veroneseSectionPolynomial r k p).Splits :=
Or.inr
(aissenSchoenbergWhitneyForward (IsPolyaFreqSeq_veroneseSectionPolynomial_of_realRooted_nonneg hpnn hprr hr hk)).1
(aissenSchoenbergWhitneyForward
(IsPolyaFreqSeq_veroneseSectionPolynomial_of_realRooted_nonneg hpnn hprr hr hk)).1

/-- Zero-aware real-rootedness of Veronese sections of real-rooted
nonnegative-coefficient polynomials, assuming both directions of ASW. -/
Expand Down
Loading