From c217bdddb2da900732d8d864991b08bf1d91a2f4 Mon Sep 17 00:00:00 2001 From: Nicolas Rouquette Date: Tue, 21 Jul 2026 05:45:30 -0400 Subject: [PATCH 1/2] chore: Bump v4.32.0 (#1445) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * chore: Bump v4.32.0 Bump lean-toolchain, mathlib, and doc-gen4 to v4.32.0 (tracker #1437) and repair the source breakages from the Mathlib 4.31->4.32 API drift across Physlib, QuantumInfo, and PhyslibAlpha. Proofs, instances, and imports only; no lemma/definition statement or mathematical content was changed. Breakage classes fixed: - Hand-rolled AddMonoid/AddCommMonoid/AddCommGroup instances whose nsmul/zsmul field proofs relied on `ring` closing scalar-multiplication (smul) goals, which it no longer does in 4.32. - Structure refactors: MonoidAlgebra and MvPolynomial are now wrapper structs (no longer defeq to their coefficient Finsupp); ContRepresentation gained a toMonoidHom field; Mathlib.Meta.Positivity.Strictness gained an Option PartialOrder index (13 positivity extensions); LeftOrdContinuous gained an s.Nonempty hypothesis. - Tactic drift in fun_prop / measurability (metavariable goals), simp / simpa / convert normal forms. - Deprecation renames: PiTensorProduct import, IsOpen.locallyPathConnectedSpace, Finset.le_eq_subset, TwoSidedIdeal.mem_ofRingCon, and the removed simpVarHead linter; def -> lemma for the propositions flagged by the defProp linter. `lake build` (Physlib + QuantumInfo + PhyslibAlpha) is green; `lake exe lint_all` and the version-bump scripts (TODO_to_yml, stats, informal, make_tag) pass. Co-authored-by: Claude Opus 4.8 * chore: address review feedback on the v4.32.0 bump Apply @nateabr's review suggestions, which simplify the migration in three places and, for the spectral measure, identify a cleaner root-cause fix: - SpaceAndTime/Space/Module.lean: define `zsmul` via `•` (`z • p.val i`), so the default `zsmul_zero'`/`zsmul_succ'`/`zsmul_neg'` proofs discharge and those blocks are dropped. - StringTheory/FTheory/SU5/Fluxes/Basic.lean: define `nsmul` via `•` and close `nsmul_zero`/`nsmul_succ` with `zero_nsmul`/`succ_nsmul`. - QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean: the 4.32 breakage was the `CoeFun` coercion, not the composition lemmas; use `⇑μS.toVectorMeasure` and revert `comp_of_disjoint`, `comp_eq_of_inter`, and `commute` to their original form. Thanks to @nateabr for the careful and constructive review. Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com> Co-authored-by: Claude Opus 4.8 * fix(QuantumMechanics): drop unused instance arguments in StinespringDilation The `unusedArguments` alpha-linter (`runPhyslibAlphaLinters`) fails under the v4.32.0 toolchain on `StinespringDilation`. The file is unchanged since the v4.31.0 bump and the same linter is green on master, so the reports are a consequence of the 4.31 -> 4.32 Mathlib bump: the matrix operations these lemmas call (`tr₂`, `stinespringOp`, `Matrix.one`) no longer thread the flagged instances through their elaborated proof terms, so the arguments are now genuinely dead. Verified against each definition's signature: - `tr₂_e₀Xe₀`: `[Zero w]` — `tr₂` needs only `[Fintype n]` on the traced index. - `tracefree_version`: `[Zero r]`, `[DecidableEq m]` — `(1 : Matrix r r R)` needs `[DecidableEq r]` (index) and `Zero/One R` (from `RCLike R`), not `Zero r`; `stinespringForm` needs `[Fintype r] [DecidableEq r] [Fintype m]`, not `[DecidableEq m]`. - `stinespringOp_apply`: `[Fintype m]`, `[DecidableEq m]` — `stinespringOp` needs only `[Fintype r] [DecidableEq r]`. - `heisenberg_schrõdinger`: `[Zero r]`, `[DecidableEq m]` — same two; these were live only because its proof (`rw [tracefree_version]`) threaded them into `tracefree_version`. CI reported only the first three; removing them from `tracefree_version` exposes this caller, which the local linter then flags. Removing instance-implicit arguments is safe for callers (they are inferred, never passed positionally). `runPhyslibAlphaLinters` is now clean. Co-Authored-By: Claude Opus 4.8 (1M context) * fix(lint): quiet 5 v4.32.0 #lint regressions on pre-existing declarations Toolchain collateral from the v4.32.0 bump — not a source change. ## Symptom The `runLinter on Physlib` CI step (`env LEAN_ABORT_ON_PANIC=1 lake exe runPhyslibLinters`, build.yml) fails on this PR with 5 errors, while the *identical* step is green on `master`. `master` still runs Lean/Mathlib v4.31.0; this PR is the v4.32.0 bump. The v4.32.0 `#lint` linters (`unusedArguments`, `checkType`) are stricter than v4.31.0's and now flag code that predates this PR. ## These are not our edits None of the 5 flagged declarations is changed by this bump: - Physlib/Relativity/Tensors/LeviCivita/Basic.lean (untouched file) - Physlib/Relativity/.../Vector/Causality/LightLike.lean (untouched file) - Physlib/SpaceAndTime/Space/Integrals/Basic.lean (untouched file) - Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (untouched file) - Physlib/Particles/.../SU5/ChargeSpectrum/Basic.lean (this PR only edits `subset_trans` at L187; the flagged `min_exists_inductive` at L333 is unchanged) ## The 5 findings and the fix 1. checkType — `leviCivita_contract_self`: whnf on its tensor-notation statement now exceeds the linter's 200k-heartbeat budget (v4.31.0 stayed under it). Statement unchanged. → `@[nolint checkType]`. 2-5. unusedArguments — `min_exists_inductive` (`hn`), `lightlike_spatial_parallel_implies_proportional` (`hv`, `hw`), `integrable_spherical_of_integrable` (`NormedSpace ℝ F`), `probability_nonneg` (`IsFiniteMeasure`, `NeZero`): each argument is part of the intended interface / goal statement but unused by the proof term. → `@[nolint unusedArguments]` (matching 17 existing uses in the tree). Consistent with this PR's charter (a toolchain bump: no lemma/definition statement or signature is added, removed, or changed), these are *silenced*, not restructured. Dropping the now-"unused" binders would alter public signatures and risk downstream breakage; that is out of scope for a bump. ## Why local `lake exe lint_all` did not catch it `scripts/lint_all.lean`'s `main` ends in an unconditional `pure 0` — it prints linter output but never sets a non-zero exit code, so it cannot gate a PR. CI does not use it; it invokes `lake exe runPhyslibLinters` directly, which *does* exit 1 on findings. Reproduce the CI gate locally with: env LEAN_ABORT_ON_PANIC=1 lake exe runPhyslibLinters Physlib Co-Authored-By: Claude Opus 4.8 (1M context) --------- Co-authored-by: Claude Opus 4.8 Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com> Co-authored-by: Claude Opus 4.8 (1M context) --- .../Kinematics/EMPotential.lean | 2 +- Physlib/Mathematics/PiTensorProduct.lean | 2 +- Physlib/Mathematics/RatComplexNum.lean | 45 ++++------------ .../SU5/ChargeSpectrum/Basic.lean | 7 ++- Physlib/QFT/AnomalyCancellation/Basic.lean | 2 +- .../FieldOpFreeAlgebra/Basic.lean | 26 ++++++---- .../FieldStatistics/Basic.lean | 8 +-- .../PerturbationTheory/WickAlgebra/Basic.lean | 4 +- .../WickContraction/Card.lean | 8 ++- .../WickContraction/InsertAndContractNat.lean | 43 ++++++++-------- .../WickContraction/Join.lean | 30 +++++------ .../WickContraction/TimeCond.lean | 8 +-- .../SpaceD/PolyBddSchwartzSubmodule.lean | 2 +- .../QuantumMechanics/Operators/Position.lean | 3 +- .../Operators/SpectralTheory/Basic.lean | 2 +- .../SpectralTheory/SpectralMeasure.lean | 2 +- .../LorentzAlgebra/ExponentialMap.lean | 4 +- .../Tensors/Contraction/SuccSuccAbove.lean | 2 +- .../Relativity/Tensors/LeviCivita/Basic.lean | 5 +- .../Vector/Causality/LightLike.lean | 3 ++ Physlib/Relativity/Tensors/Reindexing.lean | 4 +- .../SpaceAndTime/Space/Integrals/Basic.lean | 3 ++ Physlib/SpaceAndTime/Space/IsDistBounded.lean | 5 +- Physlib/SpaceAndTime/Space/Module.lean | 15 +----- .../EuclideanGroup/SchwartzAction.lean | 28 +++++----- .../CanonicalEnsemble/Basic.lean | 3 ++ .../FTheory/SU5/Fluxes/Basic.lean | 7 ++- .../TwoHDM/Invariants.lean | 5 +- .../QuantumMechanics/StinespringDilation.lean | 8 +-- QuantumInfo/Channels/MatrixMap.lean | 2 +- QuantumInfo/ClassicalInfo/Distribution.lean | 3 +- QuantumInfo/ClassicalInfo/Entropy.lean | 4 +- .../GeneralizedPerspectiveFunction.lean | 2 +- .../TraceInequality/LownerHeinzCore.lean | 10 +++- .../ForMathlib/HermitianMat/Basic.lean | 2 +- QuantumInfo/ForMathlib/HermitianMat/CFC.lean | 23 +++++---- .../ForMathlib/HermitianMat/Inner.lean | 3 +- .../ForMathlib/HermitianMat/LogExp.lean | 9 ++-- .../ForMathlib/HermitianMat/Order.lean | 51 ++++++++++++------- QuantumInfo/ForMathlib/HermitianMat/Proj.lean | 2 +- .../ForMathlib/HermitianMat/Schatten.lean | 2 +- QuantumInfo/ForMathlib/HermitianMat/Sqrt.lean | 3 +- QuantumInfo/ForMathlib/SionMinimax.lean | 42 ++++++++------- QuantumInfo/States/Mixed/MState.lean | 9 ++-- QuantumInfo/States/Pure/Braket.lean | 2 +- README.md | 2 +- lake-manifest.json | 34 ++++++------- lakefile.toml | 4 +- lean-toolchain | 2 +- 49 files changed, 256 insertions(+), 241 deletions(-) diff --git a/Physlib/Electromagnetism/Kinematics/EMPotential.lean b/Physlib/Electromagnetism/Kinematics/EMPotential.lean index b3da653ce..2e6870375 100644 --- a/Physlib/Electromagnetism/Kinematics/EMPotential.lean +++ b/Physlib/Electromagnetism/Kinematics/EMPotential.lean @@ -273,7 +273,7 @@ noncomputable instance {d} : simp smul_add Λ A B := by ext x μ - simp [Lorentz.Vector.smul_add] + simp /-! diff --git a/Physlib/Mathematics/PiTensorProduct.lean b/Physlib/Mathematics/PiTensorProduct.lean index a8bcc6cae..41e5a9bfb 100644 --- a/Physlib/Mathematics/PiTensorProduct.lean +++ b/Physlib/Mathematics/PiTensorProduct.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Mathlib.LinearAlgebra.PiTensorProduct +public import Mathlib.LinearAlgebra.PiTensorProduct.Basic /-! # Pi Tensor Products diff --git a/Physlib/Mathematics/RatComplexNum.lean b/Physlib/Mathematics/RatComplexNum.lean index 49c19f846..51dbbf123 100644 --- a/Physlib/Mathematics/RatComplexNum.lean +++ b/Physlib/Mathematics/RatComplexNum.lean @@ -83,8 +83,8 @@ instance : AddCommGroup RatComplexNum where simp · change a2 + 0 = a2 simp - nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩ neg := fun x => ⟨-x.fst, -x.snd⟩ + nsmul := fun n x => ⟨n • x.fst, n • x.snd⟩ zsmul := fun n x => ⟨n • x.1, n • x.2⟩ neg_add_cancel := by intro a @@ -102,42 +102,17 @@ instance : AddCommGroup RatComplexNum where ring · simp only [add_snd] ring - nsmul_zero := by - intro x - simp only [zero_nsmul] - rfl - nsmul_succ := by - intro x y - ext - · simp only [add_fst] - ring - · simp only [add_snd] - ring - zsmul_zero' := by - intro a - ext - · simp only [zero_smul] - rfl - · simp only [zero_smul] - rfl + nsmul_zero := by intro x; ext <;> exact zero_nsmul _ + nsmul_succ := by intro n x; ext <;> exact succ_nsmul _ _ + zsmul_zero' := by intro a; ext <;> exact zero_zsmul _ zsmul_succ' := by - intro a n - ext - · simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, zsmul_eq_mul, Int.cast_add, - Int.cast_natCast, Int.cast_one, add_fst] - ring - · simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, zsmul_eq_mul, Int.cast_add, - Int.cast_natCast, Int.cast_one, add_snd] - ring - zsmul_neg' := by - intro a n + intro n a ext - · simp only [zsmul_eq_mul, Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, - Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast, Int.cast_one] - ring - · simp only [zsmul_eq_mul, Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, - Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast, Int.cast_one] - ring + · show ((n : ℤ) + 1) • a.fst = (n : ℤ) • a.fst + a.fst + exact add_one_zsmul _ _ + · show ((n : ℤ) + 1) • a.snd = (n : ℤ) • a.snd + a.snd + exact add_one_zsmul _ _ + zsmul_neg' := by intro n a; ext <;> exact negSucc_zsmul _ _ instance : Mul RatComplexNum where mul := fun x y => ⟨x.fst * y.fst - x.snd * y.snd, x.fst * y.snd + x.snd * y.fst⟩ diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean index 7241858a8..e05fba448 100644 --- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean +++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean @@ -187,7 +187,9 @@ lemma _root_.Option.toFinset_inj {x y : Option 𝓩} : cases x <;> cases y <;> simp [Option.toFinset] lemma subset_trans {x y z : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyz : y ⊆ z) : x ⊆ z := by - simp_all [Subset] + rw [subset_def] at hxy hyz ⊢ + exact ⟨Finset.Subset.trans hxy.1 hyz.1, Finset.Subset.trans hxy.2.1 hyz.2.1, + Finset.Subset.trans hxy.2.2.1 hyz.2.2.1, Finset.Subset.trans hxy.2.2.2 hyz.2.2.2⟩ lemma subset_antisymm {x y : ChargeSpectrum 𝓩} (hxy : x ⊆ y) (hyx : y ⊆ x) : x = y := eq_of_parts @@ -328,6 +330,9 @@ lemma powerset_mono {x y : ChargeSpectrum 𝓩} : · intro h z hz exact mem_powerset_iff_subset.mpr (subset_trans (mem_powerset_iff_subset.mp hz) h) +-- `unusedArguments` (newly flagged under v4.32.0): `hn` names the induction +-- target but the proof discharges it directly via `exists_min_image`. +@[nolint unusedArguments] lemma min_exists_inductive (S : Finset (ChargeSpectrum 𝓩)) (hS : S ≠ ∅) : (n : ℕ) → (hn : S.card = n) → ∃ y ∈ S, powerset y ∩ S = {y} := by diff --git a/Physlib/QFT/AnomalyCancellation/Basic.lean b/Physlib/QFT/AnomalyCancellation/Basic.lean index 496fc4651..195bcf00b 100644 --- a/Physlib/QFT/AnomalyCancellation/Basic.lean +++ b/Physlib/QFT/AnomalyCancellation/Basic.lean @@ -227,7 +227,7 @@ instance linSolsAddCommMonoid (χ : ACCSystemLinear) : zero_add S := LinSols.ext (χ.chargesAddCommMonoid.zero_add _) add_zero S := LinSols.ext (χ.chargesAddCommMonoid.add_zero _) nsmul n S := ⟨n • S.val, fun _ ↦ by simp [S.linearSol _]⟩ - nsmul_zero n := by ext; simp only [zero_nsmul]; rfl + nsmul_zero n := LinSols.ext (χ.chargesAddCommMonoid.nsmul_zero _) nsmul_succ n S := LinSols.ext (χ.chargesAddCommMonoid.nsmul_succ _ _) /-- An instance providing the operations and properties for `LinSols` to form a diff --git a/Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean index 169c50c34..4cbec23d7 100644 --- a/Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean +++ b/Physlib/QFT/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean @@ -210,20 +210,28 @@ lemma ofFieldOpF_eq_crPartF_add_anPartF (φ : 𝓕.FieldOp) : /-- The basis of the free creation and annihilation algebra formed by lists of CrAnFieldOp. -/ noncomputable def ofCrAnListFBasis : Basis (List 𝓕.CrAnFieldOp) ℂ (FieldOpFreeAlgebra 𝓕) where - repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv + repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv ≪≫ₗ + MonoidAlgebra.coeffLinearEquiv ℂ set_option backward.isDefEq.respectTransparency false in @[simp] lemma ofListBasis_eq_ofList (φs : List 𝓕.CrAnFieldOp) : ofCrAnListFBasis φs = ofCrAnListF φs := by - simp only [ofCrAnListFBasis, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply, - Basis.coe_ofRepr, ofCrAnListF] - erw [MonoidAlgebra.lift_apply] - simp only [zero_smul, Finsupp.sum_single_index, one_smul] - rw [@FreeMonoid.lift_apply] - match φs with - | [] => rfl - | φ :: φs => erw [List.map_cons] + have key : ∀ ψs : List 𝓕.CrAnFieldOp, FreeAlgebra.equivMonoidAlgebraFreeMonoid (ofCrAnListF ψs) + = MonoidAlgebra.single (FreeMonoid.ofList ψs) 1 := by + intro ψs + induction ψs with + | nil => simp [ofCrAnListF, MonoidAlgebra.one_def] + | cons φ ψs ih => + rw [ofCrAnListF, List.map_cons, List.prod_cons, ← ofCrAnListF, map_mul, ih, + FreeMonoid.ofList_cons, + show FreeAlgebra.equivMonoidAlgebraFreeMonoid (ofCrAnOpF φ) + = MonoidAlgebra.single (FreeMonoid.of φ) 1 by + simp [ofCrAnOpF, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply], + MonoidAlgebra.single_mul_single, one_mul] + rw [Basis.apply_eq_iff] + simp only [ofCrAnListFBasis, LinearEquiv.trans_apply, AlgEquiv.toLinearEquiv_apply, key] + rfl lemma ofCrAnListF_injective : Function.Injective (ofCrAnListF (𝓕 := 𝓕)) := by intro φs φs' h diff --git a/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean b/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean index c28b361e7..dc32c1557 100644 --- a/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean +++ b/Physlib/QFT/PerturbationTheory/FieldStatistics/Basic.lean @@ -310,11 +310,11 @@ instance : AddMonoid FieldStatistic where add_assoc a b c := by cases a <;> cases b <;> cases c <;> rfl nsmul_zero a := by - simp only [Finset.univ_eq_empty, Finset.prod_const, Finset.card_empty, pow_zero] - rfl + show (∏ _i : Fin 0, a) = (1 : FieldStatistic) + rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin, pow_zero] nsmul_succ a n := by - simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin] - rfl + show (∏ _i : Fin (a + 1), n) = (∏ _i : Fin a, n) * n + simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin, pow_succ] @[simp] lemma add_eq_mul (a b : FieldStatistic) : a + b = a * b := rfl diff --git a/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean b/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean index 813ef0739..10995dfdd 100644 --- a/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean +++ b/Physlib/QFT/PerturbationTheory/WickAlgebra/Basic.lean @@ -225,7 +225,7 @@ lemma ι_eq_zero_iff_mem_ideal (x : FieldOpFreeAlgebra 𝓕) : ι x = 0 ↔ x ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by rw [ι_apply] change ⟦x⟧ = ⟦0⟧ ↔ _ - simp_all only [Quotient.eq, Con.rel_eq_coe, RingCon.toCon_coe_eq_coe, TwoSidedIdeal.mem_mk] + simp_all only [Quotient.eq, Con.rel_eq_coe, RingCon.toCon_coe_eq_coe, TwoSidedIdeal.mem_ofRingCon] lemma bosonicProjF_mem_fieldOpIdealSet_or_zero (x : FieldOpFreeAlgebra 𝓕) (hx : x ∈ 𝓕.fieldOpIdealSet) : @@ -322,7 +322,7 @@ lemma bosonicProjF_mem_ideal (x : FieldOpFreeAlgebra 𝓕) · exact TwoSidedIdeal.mem_span_iff.mpr fun I hI => hI h · simp [h] exact add_mem (add_mem (key hBy) (key hFy)) (add_mem (key hFy) (key hBy)) - · simp only [TwoSidedIdeal.mem_mk, map_zero, ZeroMemClass.coe_zero, p] + · simp only [TwoSidedIdeal.mem_ofRingCon, map_zero, ZeroMemClass.coe_zero, p] exact (RingCon.eq (ringConGen fun a b => a - b ∈ 𝓕.fieldOpIdealSet)).mp rfl · intro x y hx hy hpx hpy simp_all only [map_add, Submodule.coe_add, p] diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/Card.lean b/Physlib/QFT/PerturbationTheory/WickContraction/Card.lean index 16adb3620..d6207ba30 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/Card.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/Card.lean @@ -72,7 +72,7 @@ def consAddContract (i : Fin n.succ) (c : WickContraction n) : ⟨(c.1.map (Finset.mapEmbedding i.succAboveEmb).toEmbedding).map (Finset.mapEmbedding (Fin.succEmb n.succ)).toEmbedding ∪ {{0, i.succ}}, by intro a - simp only [succ_eq_add_one, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [succ_eq_add_one, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_exists_and_eq_and, Finset.mem_singleton] intro h rcases h with h | h @@ -86,7 +86,7 @@ def consAddContract (i : Fin n.succ) (c : WickContraction n) : simp only [succ_eq_add_one, ne_eq, and_true] exact ne_of_beq_false rfl, by intro a ha b hb - simp only [succ_eq_add_one, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [succ_eq_add_one, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_exists_and_eq_and, Finset.mem_singleton] at ha hb rcases ha with ha | ha <;> rcases hb with hb | hb · obtain ⟨a, ha, rfl⟩ := ha @@ -122,7 +122,7 @@ lemma consAddContract_getDual?_self_succ (i : Fin n.succ) (c : WickContraction n lemma mem_consAddContract_of_mem_iff (i : Fin n.succ) (c : WickContraction n) (a : Finset (Fin n)) : a ∈ c.1 ↔ (a.map i.succAboveEmb).map (Fin.succEmb n.succ) ∈ (consAddContract i c).1 := by - simp only [succ_eq_add_one, consAddContract, Finset.le_eq_subset, Finset.mem_union, + simp only [succ_eq_add_one, consAddContract, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_exists_and_eq_and, Finset.mem_singleton] apply Iff.intro · intro h @@ -186,7 +186,6 @@ lemma consAddContract_surjective_on_zero_contract (i : Fin n.succ) rw [← h2] simp · obtain ⟨b, hb, rfl⟩ := h - rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply] simp only [succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, true_and, c'] at hb exact hb · intro h @@ -207,7 +206,6 @@ lemma consAddContract_surjective_on_zero_contract (i : Fin n.succ) obtain ⟨y, rfl⟩ := (Fin.exists_succAbove_eq (x := y) (y := i)) (by omega) use {x, y} simp only [c'] - rw [Finset.mapEmbedding_apply, Finset.mapEmbedding_apply] simpa using h lemma consAddContract_bijection (i : Fin n.succ) : diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean b/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean index 25cd6b4a8..4b8716aed 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/InsertAndContractNat.lean @@ -40,7 +40,7 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c · simp only [Nat.succ_eq_add_one, f'] match j with | none => - simp only [Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding, + simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, f] intro a ha rw [Finset.mapEmbedding_apply] @@ -54,7 +54,7 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c use (i.succAbove j) simp only [ne_eq, and_true] exact Fin.ne_succAbove i j - · simp only [Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding, + · simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, f] intro a ha rw [Finset.mapEmbedding_apply] @@ -64,7 +64,7 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c simp only [Nat.succ_eq_add_one, f'] at ha hb match j with | none => - simp_all only [f, Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding, + simp_all only [f, Finset.mem_map, RelEmbedding.coe_toEmbedding, Nat.succ_eq_add_one] obtain ⟨a', ha', ha''⟩ := ha obtain ⟨b', hb', hb''⟩ := hb @@ -83,7 +83,7 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c apply Or.inr subst ha simp only [Finset.disjoint_insert_left, Finset.disjoint_singleton_left] - simp only [Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding, f] at hb + simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding, f] at hb obtain ⟨a', hb', hb''⟩ := hb subst hb'' rw [Finset.mapEmbedding_apply] @@ -102,7 +102,7 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c subst hb simp only [Finset.disjoint_insert_right, Nat.succ_eq_add_one, Finset.disjoint_singleton_right] - simp only [Finset.le_eq_subset, Finset.mem_map, RelEmbedding.coe_toEmbedding, f] at ha + simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding, f] at ha obtain ⟨a', ha', ha''⟩ := ha subst ha'' rw [Finset.mapEmbedding_apply] @@ -117,7 +117,7 @@ def insertAndContractNat (c : WickContraction n) (i : Fin n.succ) (j : Option (c subst hja exact False.elim (hj a' ha' ha) | Or.inr ha, Or.inr hb => - simp_all only [f, Finset.le_eq_subset, + simp_all only [f, or_true, Finset.mem_map, RelEmbedding.coe_toEmbedding] obtain ⟨a', ha', ha''⟩ := ha obtain ⟨b', hb', hb''⟩ := hb @@ -139,7 +139,7 @@ lemma self_mem_uncontracted_of_insertAndContractNat_none (c : WickContraction n) i ∈ (insertAndContractNat c i none).uncontracted := by rw [mem_uncontracted_iff_not_contracted] intro p hp - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_map, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_map, RelEmbedding.coe_toEmbedding] at hp obtain ⟨a, ha, ha'⟩ := hp have hc := c.2.1 a ha @@ -164,8 +164,7 @@ lemma self_not_mem_uncontracted_of_insertAndContractNat_some (c : WickContractio lemma insertAndContractNat_succAbove_mem_uncontracted_iff (c : WickContraction n) (i : Fin n.succ) (j : Fin n) : (i.succAbove j) ∈ (insertAndContractNat c i none).uncontracted ↔ j ∈ c.uncontracted := by - simp [mem_uncontracted_iff_not_contracted, insertAndContractNat, Finset.mapEmbedding_apply, - -Finset.le_eq_subset] + simp [mem_uncontracted_iff_not_contracted, insertAndContractNat, Finset.mapEmbedding_apply] @[simp] lemma mem_uncontracted_insertAndContractNat_none_iff (c : WickContraction n) (i : Fin n.succ) @@ -197,7 +196,7 @@ lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i by_cases hjz : j = z · subst hjz rw [mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, Finset.mem_insert, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, or_true, not_true_eq_false, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, false_and, ne_eq, false_iff, not_exists, not_and, Decidable.not_not] @@ -212,7 +211,7 @@ lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i rw [mem_uncontracted_iff_not_contracted] intro p hp rw [mem_uncontracted_iff_not_contracted] at h - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h have hc := h.2 p hp @@ -223,7 +222,7 @@ lemma mem_uncontracted_insertAndContractNat_some_iff (c : WickContraction n) (i rw [Function.Injective.eq_iff (Fin.succAbove_right_injective)] at hz'1 subst hz'1 rw [mem_uncontracted_iff_not_contracted] - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset, + simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding, forall_eq_or_imp, Finset.mem_singleton, not_or, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] apply And.intro @@ -279,7 +278,7 @@ lemma insertAndContractNat_succAbove_getDual?_get (c : WickContraction n) (i : F simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_map, RelEmbedding.coe_toEmbedding] exact ⟨_, self_getDual?_get_mem c j (by simpa using h), - by simp [Finset.mapEmbedding_apply, -Finset.le_eq_subset]⟩ + by simp [Finset.mapEmbedding_apply]⟩ @[simp] lemma insertAndContractNat_some_getDual?_eq (c : WickContraction n) (i : Fin n.succ) @@ -310,7 +309,7 @@ lemma insertAndContractNat_some_getDual?_ne_isSome_get (c : WickContraction n) ( Finset.mem_map, RelEmbedding.coe_toEmbedding] exact Or.inr ⟨_, self_getDual?_get_mem c k (by simpa [hkj, insertAndContractNat_some_getDual?_ne_isSome] using h), - by simp [Finset.mapEmbedding_apply, -Finset.le_eq_subset]⟩ + by simp [Finset.mapEmbedding_apply]⟩ @[simp] lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin n.succ) @@ -323,7 +322,7 @@ lemma insertAndContractNat_some_getDual?_of_neq (c : WickContraction n) (i : Fin simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] exact Or.inr ⟨{k, d}, (c.getDual?_eq_some_iff_mem k d).mp hc, - by simp [Finset.mapEmbedding_apply, -Finset.le_eq_subset]⟩ + by simp [Finset.mapEmbedding_apply]⟩ /-! @@ -339,12 +338,12 @@ lemma insertAndContractNat_erase (c : WickContraction n) (i : Fin n.succ) true_and] match j with | none => - simp [Finset.mapEmbedding_apply, Finset.map_inj, -Finset.le_eq_subset] + simp [Finset.mapEmbedding_apply, Finset.map_inj] | some j => have hn : Finset.map i.succAboveEmb a ≠ {i, i.succAbove j} := fun h => by have hi : i ∈ Finset.map i.succAboveEmb a := h ▸ Finset.mem_insert_self i _ simp [Fin.succAbove_ne] at hi - simp [Finset.mapEmbedding_apply, Finset.map_inj, hn, -Finset.le_eq_subset] + simp [Finset.mapEmbedding_apply, Finset.map_inj, hn] set_option backward.isDefEq.respectTransparency false in lemma insertAndContractNat_getDualErase (c : WickContraction n) (i : Fin n.succ) @@ -370,8 +369,7 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : match n with | 0 => apply Subtype.ext - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, insertAndContractNat, getDualErase, - Finset.le_eq_subset] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, insertAndContractNat, getDualErase] ext a simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] constructor @@ -384,8 +382,7 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : apply Subtype.ext by_cases hi : (c.getDual? i).isSome · rw [insertAndContractNat_of_isSome] - simp only [Nat.succ_eq_add_one, getDualErase, hi, ↓reduceDIte, Option.get_some, - Finset.le_eq_subset] + simp only [Nat.succ_eq_add_one, getDualErase, hi, ↓reduceDIte, Option.get_some] rw [succsAbove_predAboveI] · ext a simp only [Finset.mem_insert, Finset.mem_map, RelEmbedding.coe_toEmbedding] @@ -401,7 +398,7 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : · simp · exact (getDualErase_isSome_iff_getDual?_isSome c i).mpr hi · simp only [Nat.succ_eq_add_one, insertAndContractNat, getDualErase, hi, Bool.false_eq_true, - ↓reduceDIte, Finset.le_eq_subset] + ↓reduceDIte] ext a simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] constructor @@ -414,7 +411,7 @@ lemma erase_insert (c : WickContraction n.succ) (i : Fin n.succ) : /-- Lifts a contraction in `c` to a contraction in `(c.insert i j)`. -/ def insertLift {c : WickContraction n} (i : Fin n.succ) (j : Option (c.uncontracted)) (a : c.1) : (c.insertAndContractNat i j).1 := ⟨a.1.map (Fin.succAboveEmb i), by - simp only [Nat.succ_eq_add_one, insertAndContractNat, Finset.le_eq_subset] + simp only [Nat.succ_eq_add_one, insertAndContractNat] match j with | none => simp only [Finset.mem_map, RelEmbedding.coe_toEmbedding] diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/Join.lean b/Physlib/QFT/PerturbationTheory/WickContraction/Join.lean index 2eefa3cc7..1aba21507 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/Join.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/Join.lean @@ -35,7 +35,7 @@ def join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : WickContraction φs.length := ⟨φsΛ.1 ∪ φsucΛ.1.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding, by intro a ha - simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha rcases ha with ha | ha · exact φsΛ.2.1 a ha @@ -44,7 +44,7 @@ def join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) simp only [Finset.card_map] exact φsucΛ.2.1 a ha, by intro a ha b hb - simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha hb rcases ha with ha | ha <;> rcases hb with hb | hb · exact φsΛ.2.2 a ha b hb @@ -91,7 +91,7 @@ lemma jointLiftLeft_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction def joinLiftRight {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsucΛ.1 → (join φsΛ φsucΛ).1 := fun a => ⟨a.1.map uncontractedListEmd, by - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] right use a.1 @@ -144,7 +144,7 @@ lemma joinLift_surjective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Surjective (@joinLift _ _ φsΛ φsucΛ) := by intro a have ha2 := a.2 - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha2 rcases ha2 with ha2 | ⟨a2, ha3⟩ · use Sum.inl ⟨a, ha2⟩ @@ -173,7 +173,7 @@ lemma joinLiftLeft_or_joinLiftRight_of_mem_join {φs : List 𝓕.FieldOp} (ha : a ∈ (join φsΛ φsucΛ).1) : (∃ b, a = (joinLiftLeft (φsucΛ := φsucΛ) b).1) ∨ (∃ b, a = (joinLiftRight (φsucΛ := φsucΛ) b).1) := by - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha rcases ha with ha | ⟨a, ha, rfl⟩ · exact Or.inl ⟨⟨a, ha⟩, rfl⟩ @@ -224,7 +224,7 @@ lemma join_sndFieldOfContract_joinLift {φs : List 𝓕.FieldOp} (φsΛ : WickCo lemma mem_join_right_iff {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : Finset (Fin [φsΛ]ᵘᶜ.length)) : a ∈ φsucΛ.1 ↔ a.map uncontractedListEmd ∈ (join φsΛ φsucΛ).1 := by - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] have h1' : ¬ Finset.map uncontractedListEmd a ∈ φsΛ.1 := uncontractedListEmd_finset_not_mem a @@ -239,7 +239,7 @@ lemma mem_join_right_iff {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs. lemma join_card {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : (join φsΛ φsucΛ).1.card = φsΛ.1.card + φsucΛ.1.card := by - simp only [join, Finset.le_eq_subset] + simp only [join] rw [Finset.card_union_of_disjoint] simp only [Finset.card_map] rw [@Finset.disjoint_left] @@ -258,7 +258,7 @@ lemma join_card {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} lemma empty_join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction [empty (n := φs.length)]ᵘᶜ.length) : join empty φsΛ = congr (by simp) φsΛ := by apply Subtype.ext - simp only [join, Finset.le_eq_subset, uncontractedListEmd_empty] + simp only [join, uncontractedListEmd_empty] ext a conv_lhs => left @@ -309,7 +309,7 @@ lemma mem_join_uncontracted_of_mem_right_uncontracted {φs : List 𝓕.FieldOp} uncontractedListEmd i ∈ (join φsΛ φsucΛ).uncontracted := by rw [mem_uncontracted_iff_not_contracted] intro p hp - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at hp rcases hp with hp | hp · have hi : uncontractedListEmd i ∈ φsΛ.uncontracted := by @@ -329,7 +329,7 @@ lemma exists_mem_left_uncontracted_of_mem_join_uncontracted {φs : List 𝓕.Fie i ∈ φsΛ.uncontracted := by rw [@mem_uncontracted_iff_not_contracted] rw [@mem_uncontracted_iff_not_contracted] at ha - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at ha intro p hp simp_all @@ -345,7 +345,7 @@ lemma exists_mem_right_uncontracted_of_mem_join_uncontracted {φs : List 𝓕.Fi rw [mem_uncontracted_iff_not_contracted] at hi ⊢ intro p hp have hip := hi (p.map uncontractedListEmd) (by - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] right use p @@ -414,7 +414,7 @@ lemma join_assoc {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) ext a by_cases ha : a ∈ φsΛ.1 · simp [ha, join] - simp only [join, Finset.le_eq_subset, Finset.union_assoc, Finset.mem_union, ha, Finset.mem_map, + simp only [join, Finset.union_assoc, Finset.mem_union, ha, Finset.mem_map, RelEmbedding.coe_toEmbedding, false_or] apply Iff.intro · intro h @@ -488,7 +488,7 @@ lemma join_getDual?_apply_uncontractedListEmb_some {φs : List 𝓕.FieldOp} some (uncontractedListEmd ((φsucΛ.getDual? i).get (by simpa [join_getDual?_apply_uncontractedListEmb_isSome_iff]using hi))) := by rw [getDual?_eq_some_iff_mem] - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] right use {i, (φsucΛ.getDual? i).get (by @@ -524,7 +524,7 @@ lemma join_sub_quot (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ φsΛ.1) join (subContraction S ha) (quotContraction S ha) = φsΛ := by apply Subtype.ext ext a - simp only [join, Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] apply Iff.intro · intro h @@ -563,7 +563,7 @@ lemma join_singleton_getDual?_right {φs : List 𝓕.FieldOp} (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : (join (singleton h) φsucΛ).getDual? j = some i := by rw [@getDual?_eq_some_iff_mem] - simp only [join, singleton, Finset.le_eq_subset, Finset.mem_union, Finset.mem_singleton, + simp only [join, singleton, Finset.mem_union, Finset.mem_singleton, Finset.mem_map, RelEmbedding.coe_toEmbedding] left exact Finset.pair_comm j i diff --git a/Physlib/QFT/PerturbationTheory/WickContraction/TimeCond.lean b/Physlib/QFT/PerturbationTheory/WickContraction/TimeCond.lean index 7e3b4e4bd..c8ff80291 100644 --- a/Physlib/QFT/PerturbationTheory/WickContraction/TimeCond.lean +++ b/Physlib/QFT/PerturbationTheory/WickContraction/TimeCond.lean @@ -312,7 +312,7 @@ lemma join_eqTimeContractSet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction · intro h have hmem := mem_of_mem_eqTimeContractSet h have ht := joinLiftLeft_or_joinLiftRight_of_mem_join (φsucΛ := φsucΛ) _ hmem - simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] + simp only [Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] rcases ht with ht | ht · obtain ⟨b, rfl⟩ := ht left @@ -330,7 +330,7 @@ lemma join_eqTimeContractSet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction simp only [joinLiftRight, and_true] simpa [eqTimeContractSet] using h · intro h - simp only [Finset.le_eq_subset, Finset.mem_union, Finset.mem_map, + simp only [Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding] at h rcases h with h | h · simp only [eqTimeContractSet, Fin.getElem_fin, Finset.mem_filter, Finset.mem_univ, @@ -433,7 +433,7 @@ lemma join_haveEqTime_of_eqTimeOnly_nonEmpty {φs : List 𝓕.FieldOp} (φsΛ : (h1 : φsΛ.EqTimeOnly) (h2 : φsΛ ≠ empty) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : HaveEqTime (join φsΛ φsucΛ) := by - simp only [HaveEqTime, Fin.getElem_fin, join, Finset.le_eq_subset, Finset.mem_union, + simp only [HaveEqTime, Fin.getElem_fin, join, Finset.mem_union, Finset.mem_map, RelEmbedding.coe_toEmbedding, exists_and_left, exists_prop] simp only [EqTimeOnly, Fin.getElem_fin] at h1 obtain ⟨i, j, h⟩ := exists_pair_of_not_eq_empty _ h2 @@ -481,7 +481,7 @@ def hasEqTimeEquiv (φs : List 𝓕.FieldOp) : simp only [subContraction] rw [join_eqTimeContractSet] rw [eqTimeContractSet_of_not_haveEqTime h2] - simp only [Finset.le_eq_subset, ne_eq, Finset.map_empty, Finset.union_empty] + simp only [ne_eq, Finset.map_empty, Finset.union_empty] rw [eqTimeContractSet_of_mem_eqTimeOnly h1.1] refine hasEqTimeEquiv_ext_sigma ?_ ?_ · simp only [ne_eq] diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean index 84b547337..605e79823 100644 --- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean @@ -102,7 +102,7 @@ abbrev PolyBddSchwartzSubmodule lemma polyBddSchwartzIncl_injective {d : ℕ} (a : ℕ∞) (μ : Measure (Space d)) [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] : Function.Injective (polyBddSchwartzIncl (a := a) μ) := - LinearMap.injective_domRestrict_iff.mpr <| (schwartzIncl_ker μ).symm ▸ inf_bot_eq _ + LinearMap.injective_domRestrict_iff.mpr <| (schwartzIncl_ker μ).symm ▸ disjoint_bot_right /-- The linear equivalence between polynomially-bounded Schwartz maps and the corresponding submodule of the Hilbert space. -/ diff --git a/Physlib/QuantumMechanics/Operators/Position.lean b/Physlib/QuantumMechanics/Operators/Position.lean index 1b5aaee0d..97b461be4 100644 --- a/Physlib/QuantumMechanics/Operators/Position.lean +++ b/Physlib/QuantumMechanics/Operators/Position.lean @@ -176,7 +176,8 @@ lemma radiusPowLM_apply_contDiffAt {d : ℕ} (s : ℝ) (n : ℕ∞) (ψ : 𝓢(S lemma radiusPowLM_apply_stronglyMeasurable {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) : StronglyMeasurable (𝐫 s ψ) := by rw [radiusPowLM_apply_fun] - exact StronglyMeasurable.smul (by measurability) ψ.continuous.stronglyMeasurable + exact StronglyMeasurable.smul (f := fun x : Space d => ‖x‖ ^ s) (by measurability) + ψ.continuous.stronglyMeasurable /-- `x ↦ ‖x‖ˢψ(x)` is square-integrable provided `s` is not too negative. -/ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : ℕ) diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean b/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean index 510d9c549..a9b138010 100644 --- a/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean +++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean @@ -418,7 +418,7 @@ lemma IsClosable.defectNumber_const [CompleteSpace H] T.defectNumber z₁ = T.defectNumber z₂ := by by_cases hz₁ : z₁ ∈ T.regularityDomain · have h_joined : JoinedIn T.regularityDomain z₁ z₂ := by - haveI := T.regularityDomain_isOpen.locPathConnectedSpace + haveI := T.regularityDomain_isOpen.locallyPathConnectedSpace have hz₂ : z₂ ∈ T.regularityDomain := connectedComponentIn_subset _ _ hz apply (joinedIn_iff_joined hz₁ hz₂).mpr rw [← mem_pathComponent_iff, pathComponent_eq_connectedComponent] diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean b/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean index 40933eafa..ca653f883 100644 --- a/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean +++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean @@ -76,7 +76,7 @@ instance instCoeVectorMeasure : Coe (SpectralMeasure α H) (VectorMeasure α (H ⟨toVectorMeasure⟩ instance instCoeFun : CoeFun (SpectralMeasure α H) fun _ ↦ Set α → H →L[ℂ] H := - ⟨fun μS ↦ μS.toVectorMeasure.measureOf'⟩ + ⟨fun μS ↦ ⇑μS.toVectorMeasure⟩ lemma isStarProjection (A : Set α) : IsStarProjection (μS A) := μS.isStarProjection' A diff --git a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean index a906c0aab..3b2b8b639 100644 --- a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean +++ b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean @@ -145,9 +145,7 @@ theorem exp_isOrthochronous (A : lorentzAlgebra) : let γ : Path (0 : lorentzAlgebra) A := { toFun := fun t => t.val • A, continuous_toFun := by - apply Continuous.smul - · exact continuous_subtype_val - · exact continuous_const, + exact Continuous.smul continuous_subtype_val continuous_const, source' := by simp [zero_smul], target' := by simp [one_smul] } let exp_γ : Path (1 : LorentzGroup 3) ⟨NormedSpace.exp A.1, exp_mem_lorentzGroup A⟩ := diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index 8b6eefa7a..d5e1a0a6d 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -167,7 +167,7 @@ lemma succSuccAbove_symm (i j : Fin (n + 1 + 1)) : grind (splits := 5) set_option warning.simp.varHead false in -@[simp, nolint simpVarHead] +@[simp] lemma apply_succSuccAbove_symm {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1)) (k : Fin n) : c (succSuccAbove i j k) = c (succSuccAbove j i k) := by rw [succSuccAbove_symm] diff --git a/Physlib/Relativity/Tensors/LeviCivita/Basic.lean b/Physlib/Relativity/Tensors/LeviCivita/Basic.lean index fb1eb133d..09d8f3fde 100644 --- a/Physlib/Relativity/Tensors/LeviCivita/Basic.lean +++ b/Physlib/Relativity/Tensors/LeviCivita/Basic.lean @@ -164,7 +164,10 @@ lemma leviCivita_contract_three : {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ( (-6) • unitTensor (S := realLorentzTensor) Color.down | σ τ }ᵀ := by sorry -@[sorryful] +-- `checkType` linter: under the v4.32.0 toolchain, whnf on this tensor-notation +-- statement exceeds the linter's 200k-heartbeat budget (it did not on v4.31.0). +-- Statement unchanged; see the v4.32.0 bump commit message. +@[sorryful, nolint checkType] lemma leviCivita_contract_self : {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toField = - 24 := by sorry diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/LightLike.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/LightLike.lean index c919ddf4f..26bc4b31a 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/LightLike.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/LightLike.lean @@ -52,6 +52,9 @@ lemma lightlike_eq_spatial_norm_of_eq_time {d : ℕ} {v w : Vector d} set_option linter.unusedVariables false in /-- If two lightlike vectors have parallel spatial components, their temporal components must also be proportional, which implies the entire vectors are proportional -/ +-- `unusedArguments` (newly flagged under v4.32.0): the lightlike hypotheses are +-- part of the intended interface but not needed by the current proof. +@[nolint unusedArguments] lemma lightlike_spatial_parallel_implies_proportional {d : ℕ} {v w : Vector d} (hv : causalCharacter v = .lightLike) (hw : causalCharacter w = .lightLike) (h_spatial_parallel : ∃ (r : ℝ), v = r • w) : diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 828c889f5..8c81e7ce6 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -118,7 +118,7 @@ lemma preserve_color {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} rw [h.2] set_option warning.simp.varHead false in -@[simp, nolint simpVarHead] +@[simp] lemma inv_perserve_color {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : IsReindexing c c1 σ) (x : Fin n) : c1 (h.inv σ x) = c x := by @@ -129,7 +129,7 @@ lemma inv_perserve_color {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} rfl set_option warning.simp.varHead false in -@[simp, nolint simpVarHead] +@[simp] lemma toEquiv_symm_perserve_color {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} {σ : Fin m → Fin n} (h : IsReindexing c c1 σ) (x : Fin m) : c (h.toEquiv.symm x) = c1 x := by diff --git a/Physlib/SpaceAndTime/Space/Integrals/Basic.lean b/Physlib/SpaceAndTime/Space/Integrals/Basic.lean index 1a957df94..fbaf4b324 100644 --- a/Physlib/SpaceAndTime/Space/Integrals/Basic.lean +++ b/Physlib/SpaceAndTime/Space/Integrals/Basic.lean @@ -120,6 +120,9 @@ lemma integral_volume_eq_spherical (d : ℕ) [NeZero d] (f : Space d → F) field_simp simp +-- `unusedArguments` (newly flagged under v4.32.0): `NormedSpace ℝ F` is required +-- to state the goal but is not referenced in the proof term. +@[nolint unusedArguments] lemma integrable_spherical_of_integrable {d : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Space d → F} (hf : Integrable f volume) : diff --git a/Physlib/SpaceAndTime/Space/IsDistBounded.lean b/Physlib/SpaceAndTime/Space/IsDistBounded.lean index d1cae0576..e977aef5c 100644 --- a/Physlib/SpaceAndTime/Space/IsDistBounded.lean +++ b/Physlib/SpaceAndTime/Space/IsDistBounded.lean @@ -901,14 +901,15 @@ lemma component_mul_isDistBounded {d : ℕ} {f : Space d → ℝ} lemma isDistBounded_smul_self {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => f x • x) := by refine IsDistBounded.congr (f := fun x => ‖x‖ * f x) (by fun_prop) - (AEStronglyMeasurable.smul (by fun_prop) (by fun_prop)) fun x => ?_ + (AEStronglyMeasurable.smul (f := f) (g := fun x => x) (by fun_prop) (by fun_prop)) fun x => ?_ simp [norm_smul, mul_comm] @[fun_prop] lemma isDistBounded_smul_self_repr {d : ℕ} {f : Space d → ℝ} (hf : IsDistBounded f) : IsDistBounded (fun x => f x • basis.repr x) := by refine IsDistBounded.congr (f := fun x => ‖x‖ * f x) (by fun_prop) - (AEStronglyMeasurable.smul (by fun_prop) (by fun_prop)) fun x => ?_ + (AEStronglyMeasurable.smul (f := f) (g := fun x => basis.repr x) (by fun_prop) (by fun_prop)) + fun x => ?_ simp [norm_smul, mul_comm] @[fun_prop] diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 9c33f63de..e676fc4c8 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/Physlib/SpaceAndTime/Space/Module.lean @@ -192,23 +192,10 @@ lemma neg_apply {d : ℕ} (p : Space d) (i : Fin d) : (-p) i = - (p i) := by rfl noncomputable instance {d} : AddCommGroup (Space d) where - zsmul z p := ⟨fun i => z * p.val i⟩ + zsmul z p := ⟨fun i => z • p.val i⟩ neg_add_cancel p := by ext i simp - zsmul_zero' p := by - ext i - simp - zsmul_succ' n p := by - ext i - simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, Int.cast_add, Int.cast_natCast, - Int.cast_one, add_apply] - ring - zsmul_neg' n p := by - ext i - simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, Nat.succ_eq_add_one, - Int.cast_add, Int.cast_natCast, Int.cast_one, neg_apply] - ring @[simp] lemma sub_apply {d} (p q : Space d) (i : Fin d) : diff --git a/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean b/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean index e4e3b76ef..b289e5058 100644 --- a/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean +++ b/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean @@ -59,19 +59,21 @@ plain mathlib `Representation` (`G →* V →ₗ[ℝ] V`) is recovered via `ContRepresentation.toRepresentation`. -/ noncomputable def schwartzEuclideanAction {d : ℕ} : ContRepresentation ℝ (EuclideanGroup d) 𝓢(TimeAndSpace d, F) where - toFun g := SchwartzMap.compCLMOfAntilipschitz (𝕜 := ℝ) - (g := fun tx : TimeAndSpace d => g⁻¹ • tx) - (TimeAndSpace.smul_hasTemperateGrowth g⁻¹) - (TimeAndSpace.antilipschitz_smul g⁻¹) - map_one' := by - ext η tx - simp - map_mul' g h := by - ext η tx - simp only [_root_.mul_inv_rev, SchwartzMap.compCLMOfAntilipschitz_apply, - Function.comp_apply] - rw [mul_smul] - rfl + toMonoidHom := + { toFun := fun g => SchwartzMap.compCLMOfAntilipschitz (𝕜 := ℝ) + (g := fun tx : TimeAndSpace d => g⁻¹ • tx) + (TimeAndSpace.smul_hasTemperateGrowth g⁻¹) + (TimeAndSpace.antilipschitz_smul g⁻¹) + map_one' := by + ext η tx + simp + map_mul' := by + intro g h + ext η tx + simp only [_root_.mul_inv_rev, SchwartzMap.compCLMOfAntilipschitz_apply, + Function.comp_apply] + rw [mul_smul] + rfl } /-- Pointwise formula for the monoid-homomorphism form of the Schwartz-map pullback action. -/ @[simp] diff --git a/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean b/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean index 6e2992d85..a2df56b9d 100644 --- a/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean +++ b/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean @@ -566,6 +566,9 @@ noncomputable def differentialEntropy (T : Temperature) : ℝ := - kB * ∫ i, log (probability 𝓒 T i) ∂𝓒.μProd T /-- Probabilities are non-negative, assuming a positive partition function. -/ +-- `unusedArguments` (newly flagged under v4.32.0): the finiteness / non-zero +-- instances are part of the intended interface but not needed by this proof. +@[nolint unusedArguments] lemma probability_nonneg (T : Temperature) [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ] (i : ι) : 0 ≤ 𝓒.probability T i := diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean index ed6c30520..89c157a52 100644 --- a/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean +++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean @@ -205,10 +205,9 @@ instance : AddCommMonoid Fluxes where zero_add f := Fluxes.ext_iff.mpr <| by simp add_zero f := Fluxes.ext_iff.mpr <| by simp add_comm f1 f2 := Fluxes.ext_iff.mpr <| by simp only [add_M, add_N]; ring_nf; simp - nsmul n f := ⟨n * f.M, n * f.N⟩ - nsmul_zero f := Fluxes.ext_iff.mpr <| by simp - nsmul_succ n f := Fluxes.ext_iff.mpr <| by - simp only [Nat.cast_add, Nat.cast_one, add_M, add_N]; ring_nf; simp + nsmul n f := ⟨n • f.M, n • f.N⟩ + nsmul_zero f := Fluxes.ext_iff.mpr ⟨zero_nsmul f.M, zero_nsmul f.N⟩ + nsmul_succ n f := Fluxes.ext_iff.mpr ⟨succ_nsmul f.M n, succ_nsmul f.N n⟩ end Fluxes diff --git a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean index d547143b1..cd736e10d 100644 --- a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean +++ b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean @@ -566,11 +566,12 @@ lemma eval_Qslice_eigenPoint (P : MvPolynomial (Fin 6) ℝ) (X : Fin 4 → ℝ) open MvPolynomial in /-- The real part of a complex polynomial, taken coefficient-wise. -/ noncomputable def realPart (H : MvPolynomial (Fin 5) ℂ) : MvPolynomial (Fin 5) ℝ := - Finsupp.mapRange Complex.re Complex.zero_re H + .ofCoeff (Finsupp.mapRange Complex.re Complex.zero_re (AddMonoidAlgebra.coeff H)) open MvPolynomial in @[simp] lemma realPart_coeff (H : MvPolynomial (Fin 5) ℂ) (m : Fin 5 →₀ ℕ) : - coeff m (realPart H) = (coeff m H).re := Finsupp.mapRange_apply + coeff m (realPart H) = (coeff m H).re := by + simp only [realPart, coeff, AddMonoidAlgebra.coeff_ofCoeff, Finsupp.mapRange_apply] open MvPolynomial in lemma realPart_C (a : ℂ) : realPart (C a) = C a.re := by diff --git a/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean b/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean index 6dfa6950b..fd8431e44 100644 --- a/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean +++ b/PhyslibAlpha/QuantumMechanics/StinespringDilation.lean @@ -501,7 +501,7 @@ open Kronecker TensorProduct /-- Taking the partial trace of a tensor product with a matrix of trace 1 is the identity map. -/ lemma tr₂_e₀Xe₀ {R : Type*} [RCLike R] - {m w : Type*} [Fintype w] [Zero w] + {m w : Type*} [Fintype w] (e : Matrix w w R) (htr : e.trace = 1) (ρ : Matrix m m R) : tr₂ (ρ ⊗ₖ e) = ρ := by @@ -536,7 +536,7 @@ def stinespringUnitaryForm_e {R : Type*} [RCLike R] {m r : ℕ} /-- Trace-free version of the Stinespring Dilation Theorem. -/ theorem tracefree_version {R : Type*} [RCLike R] - {m r : Type*} [Fintype r] [DecidableEq r] [Zero r] [Fintype m] [DecidableEq m] + {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] {K : r → Matrix m m R} (ρ : Matrix m m R) : let K' := fun i x y => star <| K i y x; let U := (stinespringOp K'); @@ -556,7 +556,7 @@ theorem tracefree_version {R : Type*} [RCLike R] /-- A Heisberg picture / Schrödinger picture view of the Stinespring dilation. -/ theorem heisenberg_schrõdinger {R : Type*} [RCLike R] - {m r : Type*} [Fintype r] [DecidableEq r] [Zero r] [Fintype m] [DecidableEq m] + {m r : Type*} [Fintype r] [DecidableEq r] [Fintype m] {K : r → Matrix m m R} (ρ : Matrix m m R) : let K' := fun i x y => star <| K i y x @@ -722,7 +722,7 @@ def krausCompletion {R : Type*} [RCLike R] {m r : ℕ} /-- Entrywise formula for the Stinespring isometry: its `((x₁, x₂), y)` entry is `K x₂ x₁ y`. -/ theorem stinespringOp_apply {R : Type*} [Ring R] {m r : Type*} [Fintype r] [DecidableEq r] - [Fintype m] [DecidableEq m] (K : r → Matrix m m R) (x : m × r) (y : m) : + (K : r → Matrix m m R) (x : m × r) (y : m) : stinespringOp K x y = K x.2 x.1 y := by unfold stinespringOp simp [Matrix.sum_apply, Matrix.kroneckerMap_apply, Matrix.single_apply] diff --git a/QuantumInfo/Channels/MatrixMap.lean b/QuantumInfo/Channels/MatrixMap.lean index c5eea82a5..0ef65f9fd 100644 --- a/QuantumInfo/Channels/MatrixMap.lean +++ b/QuantumInfo/Channels/MatrixMap.lean @@ -6,7 +6,7 @@ Authors: Alex Meiburg module public import Mathlib.LinearAlgebra.TensorProduct.Matrix -public import Mathlib.LinearAlgebra.PiTensorProduct +public import Mathlib.LinearAlgebra.PiTensorProduct.Basic public import Mathlib.LinearAlgebra.PiTensorProduct.Basis public import Mathlib.Data.Set.Card public import Mathlib.Algebra.Module.LinearMap.Basic diff --git a/QuantumInfo/ClassicalInfo/Distribution.lean b/QuantumInfo/ClassicalInfo/Distribution.lean index 7ec3fd2f0..9f81677cb 100644 --- a/QuantumInfo/ClassicalInfo/Distribution.lean +++ b/QuantumInfo/ClassicalInfo/Distribution.lean @@ -303,9 +303,10 @@ def congrRandVar (σ : α ≃ β) : RandVar α T ≃ RandVar β T := by · simp [Function.comp_assoc] · rw [← ProbDistribution.congr_symm_apply, Equiv.apply_symm_apply] +omit inst in /-- Given a `T`-valued random variable `X` over `α`, mapping over `T` commutes with the equivalence over `α` -/ -def map_congr_eq_congr_map {S : Type _} [Mixable U S] (f : T → S) (σ : α ≃ β) (X : RandVar α T) : +lemma map_congr_eq_congr_map {S : Type _} [Mixable U S] (f : T → S) (σ : α ≃ β) (X : RandVar α T) : f <$> congrRandVar σ X = congrRandVar σ (f <$> X) := by rfl /-- The expectation value is invariant under equivalence of random variables -/ diff --git a/QuantumInfo/ClassicalInfo/Entropy.lean b/QuantumInfo/ClassicalInfo/Entropy.lean index c7f579ad7..95d18bf39 100644 --- a/QuantumInfo/ClassicalInfo/Entropy.lean +++ b/QuantumInfo/ClassicalInfo/Entropy.lean @@ -31,12 +31,12 @@ def H₁ : Prob → ℝ := /-- H₁ of 0 is zero.-/ @[simp] -def H₁_zero_eq_zero : H₁ 0 = 0 := by +lemma H₁_zero_eq_zero : H₁ 0 = 0 := by simp [H₁] /-- H₁ of 1 is zero.-/ @[simp] -def H₁_one_eq_zero : H₁ 1 = 0 := by +lemma H₁_one_eq_zero : H₁ 1 = 0 := by simp [H₁] /-- Entropy is nonnegative. -/ diff --git a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/GeneralizedPerspectiveFunction.lean b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/GeneralizedPerspectiveFunction.lean index d92d8e73c..e5bd68b95 100644 --- a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/GeneralizedPerspectiveFunction.lean +++ b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/GeneralizedPerspectiveFunction.lean @@ -529,7 +529,7 @@ theorem theorem_2_6_forward_jointlyConcaveOn_psd_pd_Ici refine ⟨?_, ?_, ?_⟩ · intro K _ _ _ _ exact (hfconc (K := K)) - · simpa using hfcont.neg + · exact hfcont.neg · simpa using (neg_nonpos.mpr hf0) have hconv_neg : JointlyConvexOn (psdSet (ℋ := ℋ)) (pdSet (ℋ := ℋ)) diff --git a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LownerHeinzCore.lean b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LownerHeinzCore.lean index 93674e3e5..ee5720dc0 100644 --- a/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LownerHeinzCore.lean +++ b/QuantumInfo/ForMathlib/HayataGroup/TraceInequality/LownerHeinzCore.lean @@ -700,7 +700,10 @@ theorem ratio_add_t_operatorMonotoneOn_Ici : ∀ (t : ℝ), 0 < t → simpa [Set.Ici] using (hspT hx) exact ne_of_gt (add_pos_of_nonneg_of_pos hx0 ht) have hT_cont : ContinuousOn invfun (spectrum ℝ T) := by - simpa [invfun, one_div] using (continuousOn_id.add continuousOn_const).inv₀ hT_ne0 + have h1 : ContinuousOn (fun x : ℝ ↦ x + t) (spectrum ℝ T) := + continuousOn_id.add continuousOn_const + have h2 : ContinuousOn (fun x : ℝ ↦ (x + t)⁻¹) (spectrum ℝ T) := h1.inv₀ hT_ne0 + simpa [invfun, one_div] using h2 dsimp [cfcR] have hcongr : cfcR (fun x : ℝ ↦ x / (x + t)) T = @@ -765,7 +768,10 @@ theorem ratio_add_t_operatorConcaveOn_Ici : ∀ (t : ℝ), 0 < t → simpa [Set.Ici] using (Ts hx) exact ne_of_gt (add_pos_of_nonneg_of_pos hx0 ht) have hcont : ContinuousOn invfun (spectrum ℝ T) := by - simpa [invfun, one_div] using (continuousOn_id.add continuousOn_const).inv₀ hne0 + have h1 : ContinuousOn (fun x : ℝ ↦ x + t) (spectrum ℝ T) := + continuousOn_id.add continuousOn_const + have h2 : ContinuousOn (fun x : ℝ ↦ (x + t)⁻¹) (spectrum ℝ T) := h1.inv₀ hne0 + simpa [invfun, one_div] using h2 dsimp [cfcR] have hcongr : cfcR (fun x : ℝ ↦ - (x / (x + t))) T diff --git a/QuantumInfo/ForMathlib/HermitianMat/Basic.lean b/QuantumInfo/ForMathlib/HermitianMat/Basic.lean index 31eaa84ad..361c2ff8c 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Basic.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Basic.lean @@ -305,7 +305,7 @@ theorem one_zpow : ((1 : HermitianMat m α) ^ z) = 1 := by ext1; simp @[simp] -theorem zpow_neg_one : A ^ (-1) = A⁻¹ := by +theorem zpow_neg_one : A ^ (-1 : ℤ) = A⁻¹ := by ext1; exact A.mat.zpow_neg_one @[simp] diff --git a/QuantumInfo/ForMathlib/HermitianMat/CFC.lean b/QuantumInfo/ForMathlib/HermitianMat/CFC.lean index 663525d84..ea6750ad1 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/CFC.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/CFC.lean @@ -848,17 +848,18 @@ lemma dist_lt_of_continuous_spectrum {X : Type*} [TopologicalSpace X] intro i generalize_proofs at *; ( have h_cont : ContinuousWithinAt (fun p : X × ℝ => f p.1 p.2 - f x₀ p.2) (S ×ˢ T) (x₀, (A x₀).H.eigenvalues i) := by - have := hf (x₀, (A x₀).H.eigenvalues i) ⟨hx₀, ?_⟩ - generalize_proofs at *; - · convert this.sub ( ContinuousWithinAt.comp ( show ContinuousWithinAt ( fun p : ℝ => f x₀ p ) T ( ( A x₀ ).H.eigenvalues i ) from ?_ ) ( continuousWithinAt_snd ) ?_ ) using 1 <;> norm_num +zetaDelta at *; - · have := hf ( x₀, ( A x₀ ).H.eigenvalues i ) ⟨ hx₀, hA₁ x₀ hx₀ ((A x₀).H.eigenvalues_mem_spectrum_real i) ⟩ - generalize_proofs at *; ( - convert! this.comp ( show ContinuousWithinAt ( fun p => ( x₀, p ) ) T ( ( A x₀ ).H.eigenvalues i ) from ?_ ) ?_ using 1 ; - generalize_proofs at *; ( - exact ContinuousWithinAt.prodMk ( continuousWithinAt_const ) (continuousWithinAt_id)); - exact fun x hx => ⟨ hx₀, hx ⟩); - · exact fun x hx => hx.2; - · exact hA₁ x₀ hx₀ ((A x₀).H.eigenvalues_mem_spectrum_real i) ) + have hmemT : (A x₀).H.eigenvalues i ∈ T := + hA₁ x₀ hx₀ ((A x₀).H.eigenvalues_mem_spectrum_real i) + have h1 : ContinuousWithinAt (fun p : X × ℝ => f p.1 p.2) (S ×ˢ T) + (x₀, (A x₀).H.eigenvalues i) := hf (x₀, (A x₀).H.eigenvalues i) ⟨hx₀, hmemT⟩ + have hg : ContinuousWithinAt (fun q : ℝ => f x₀ q) T ((A x₀).H.eigenvalues i) := + (hf (x₀, (A x₀).H.eigenvalues i) ⟨hx₀, hmemT⟩).comp + (continuousWithinAt_const.prodMk continuousWithinAt_id) (fun q hq => ⟨hx₀, hq⟩) + have h2 : ContinuousWithinAt (fun p : X × ℝ => f x₀ p.2) (S ×ˢ T) + (x₀, (A x₀).H.eigenvalues i) := + hg.comp (f := Prod.snd) (x := (x₀, (A x₀).H.eigenvalues i)) + continuousWithinAt_snd (fun p hp => hp.2) + exact h1.sub h2 ) generalize_proofs at *; ( have := h_cont.eventually ( Metric.ball_mem_nhds _ hε ) simp_all [ dist_eq_norm ] diff --git a/QuantumInfo/ForMathlib/HermitianMat/Inner.lean b/QuantumInfo/ForMathlib/HermitianMat/Inner.lean index a7278fad0..8320138c7 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Inner.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Inner.lean @@ -378,8 +378,7 @@ noncomputable instance : NormedAddCommGroup (HermitianMat d ℂ) := --PR'ed in #35056 open ComplexOrder in -@[reducible] -def _root_.RCLike.instOrderClosed : OrderClosedTopology 𝕜 where +lemma _root_.RCLike.instOrderClosed : OrderClosedTopology 𝕜 where isClosed_le' := by conv => enter [1, 1, p]; rw [RCLike.le_iff_re_im] simp_rw [Set.setOf_and] diff --git a/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean b/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean index 36063f7c9..951da6564 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/LogExp.lean @@ -84,7 +84,8 @@ TODO: We could add a fallback to give `nonnegative` if `Nonempty d` is not avail possibly also print a warning. (Users might often not have `Nonempty d` in context, and they probably want to.) -/ @[positivity HermitianMat.exp _] -meta def evalHermitianMatExp : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatExp : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app _exp (A : Expr) ← whnfR e | throwError "not HermitianMat.exp" pure (.positive (← mkAppM ``HermitianMat.exp_pos #[A])) @@ -215,7 +216,8 @@ theorem logApprox_mono {x y : HermitianMat d 𝕜} (hx : x.mat.PosDef) (hy : y.m ∫ t in (0)..T, ((1 + t)⁻¹ • (1 : HermitianMat d 𝕜) - (y + t • 1)⁻¹) := by -- By the properties of the integral, we can bring the limit inside, so we have: have h_integrable : ContinuousOn (fun t : ℝ => (1 + t)⁻¹ • (1 : HermitianMat d 𝕜)) (Set.Icc 0 T) ∧ ContinuousOn (fun t : ℝ => (x + t • 1)⁻¹) (Set.Icc 0 T) ∧ ContinuousOn (fun t : ℝ => (y + t • 1)⁻¹) (Set.Icc 0 T) := by - refine' ⟨ ContinuousOn.smul ( ContinuousOn.inv₀ ( continuousOn_const.add continuousOn_id ) fun t ht => by linarith [ ht.1 ] ) continuousOn_const, _, _ ⟩; + refine' ⟨ ContinuousOn.smul ( ContinuousOn.inv₀ ( continuousOn_const.add continuousOn_id ) fun t ht => by + simp only [Pi.add_apply, id_eq]; linarith [ ht.1 ] ) continuousOn_const, _, _ ⟩; · refine' ContinuousOn.comp ( show ContinuousOn ( fun m : HermitianMat d 𝕜 => m⁻¹ ) ( { m : HermitianMat d 𝕜 | m.mat.PosDef } ) from _ ) _ _; · intro m hm; refine' ContinuousAt.continuousWithinAt _; @@ -588,7 +590,8 @@ theorem logApprox_concave {n 𝕜 : Type*} [Fintype n] [DecidableEq n] [RCLike have h_integrable := integrable_inv_shift hz T hT rw [ intervalIntegrable_iff_integrableOn_Ioc_of_le hT ] at * refine MeasureTheory.Integrable.sub ?_ h_integrable - exact ContinuousOn.integrableOn_Icc ( by exact continuousOn_of_forall_continuousAt fun t ht => ContinuousAt.smul ( ContinuousAt.inv₀ ( continuousAt_const.add continuousAt_id ) ( by linarith [ ht.1 ] ) ) continuousAt_const ) |> fun h => h.mono_set ( Set.Ioc_subset_Icc_self ); + exact ContinuousOn.integrableOn_Icc ( by exact continuousOn_of_forall_continuousAt fun t ht => ContinuousAt.smul ( ContinuousAt.inv₀ ( continuousAt_const.add continuousAt_id ) ( by + simp only [Pi.add_apply, id_eq]; linarith [ ht.1 ] ) ) continuousAt_const ) |> fun h => h.mono_set ( Set.Ioc_subset_Icc_self ); have h_int2 : IntervalIntegrable (fun t => (1 + t)⁻¹ • (1 : HermitianMat n 𝕜) - ((a • x + b • y) + t • 1)⁻¹) MeasureTheory.volume 0 T := by exact h_integrable (Matrix.PosDef.Convex hx hy ha hb hab) have h_integral_mono : ∫ t in (0)..T, a • ((1 + t)⁻¹ • (1 : HermitianMat n 𝕜) - (x + t • 1)⁻¹) + b • ((1 + t)⁻¹ • (1 : HermitianMat n 𝕜) - (y + t • 1)⁻¹) ≤ ∫ t in (0)..T, (1 + t)⁻¹ • (1 : HermitianMat n 𝕜) - ((a • x + b • y) + t • 1)⁻¹ := by diff --git a/QuantumInfo/ForMathlib/HermitianMat/Order.lean b/QuantumInfo/ForMathlib/HermitianMat/Order.lean index 5f31efe28..b4de4348a 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Order.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Order.lean @@ -94,13 +94,16 @@ open Lean Meta Mathlib.Meta.Positivity in /-- Positivity extension for `HermitianMat.trace`: nonneg when the matrix is nonneg, positive when the matrix is positive. -/ @[positivity HermitianMat.trace _] -meta def evalHermitianMatTrace : PositivityExt where eval {_u _α} _zα _pα e := do - let .app _tr (A : Expr) ← whnfR e | throwError "not HermitianMat.trace" - let (isStrict, pfA) ← bestResult A - if isStrict then - pure (.positive (← mkAppM ``HermitianMat.trace_pos #[pfA])) - else - pure (.nonnegative (← mkAppM ``HermitianMat.trace_nonneg #[pfA])) +meta def evalHermitianMatTrace : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with + | none => pure .none + | some _ => do + let .app _tr (A : Expr) ← whnfR e | throwError "not HermitianMat.trace" + let (isStrict, pfA) ← bestResult A + if isStrict then + pure (.positive (← mkAppM ``HermitianMat.trace_pos #[pfA])) + else + pure (.nonnegative (← mkAppM ``HermitianMat.trace_nonneg #[pfA])) --Without these shortcut instances, `gcongr` fails to close certain goals...? Why? TODO instance : PosSMulMono ℝ (HermitianMat n 𝕜) := inferInstance @@ -216,9 +219,10 @@ open Lean Meta Mathlib.Meta.Positivity in /-- Positivity extension for `Matrix`: looks for `A.PosSemidef` or `A.PosDef` in the local context (including syntactic `And` conjunctions) to prove `0 ≤ A` or `0 < A`. -/ @[positivity (_ : HermitianMat _ _)] -meta def evalMatrixPSD : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalMatrixPSD : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _pα => do let lctx ← getLCtx - let mut best : Strictness _zα _pα e := .none + let mut best : Strictness _zα e (some _pα) := .none for ldecl in lctx do if ldecl.isImplementationDetail then continue let ty := ldecl.type @@ -293,10 +297,11 @@ open Lean Meta Mathlib.Meta.Positivity in /-- Positivity extension for `HermitianMat`: looks for `A.mat.PosSemidef` or `A.mat.PosDef` in the local context (including syntactic `And` conjunctions) to prove `0 ≤ A` or `0 < A`. -/ @[positivity (_ : HermitianMat _ _)] -meta def evalHermitianMatPSD : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatPSD : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _pα => do trace[Tactic.positivity] "evalHermitianMatPSD: {e}" let lctx ← getLCtx - let mut best : Strictness _zα _pα e := .none + let mut best : Strictness _zα e (some _pα) := .none for ldecl in lctx do if ldecl.isImplementationDetail then continue let ty := ldecl.type @@ -313,7 +318,8 @@ meta def evalHermitianMatPSD : PositivityExt where eval {_u _α} _zα _pα e := open Lean Meta Mathlib.Meta.Positivity in /-- Positivity extension for `HermitianMat.kronecker`: nonneg when both factors are. -/ @[positivity HermitianMat.kronecker _ _] -meta def evalHermitianMatKronecker : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatKronecker : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app (.app _kron A) B ← whnfR e | throwError "not HermitianMat.kronecker" let (isStrictA, pfA) ← bestResult A let (isStrictB, pfB) ← bestResult B @@ -339,7 +345,8 @@ theorem conj_pos [DecidableEq n] {A : HermitianMat n 𝕜} {M : Matrix m n 𝕜} open Lean Meta Mathlib.Meta.Positivity in /-- Positivity extension for `HermitianMat.conj`: nonneg when the inner matrix is. -/ @[positivity HermitianMat.conj _ _] -meta def evalHermitianMatConj : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatConj : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app (.app _coe conjM) (A : Expr) ← whnfR e | throwError "not conj application" let M := conjM.appArg! let (_, pfA) ← bestResult A @@ -584,7 +591,8 @@ private theorem _root_.Matrix.eigenvalues_nonneg [DecidableEq n] {M : Matrix n n /-- Positivity extension for `A.mat` where `A : HermitianMat`: nonneg when `0 ≤ A`. -/ @[positivity HermitianMat.mat _] -meta def evalHermitianMatMat : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatMat : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app _matFn (A : Expr) ← whnfR e | throwError "not HermitianMat.mat" match ← bestResult A with | (true, pa) => @@ -594,7 +602,8 @@ meta def evalHermitianMatMat : PositivityExt where eval {_u _α} _zα _pα e := /-- Positivity extension for `A.mat` where `A : HermitianMat`: nonneg when `0 ≤ A`. -/ @[positivity Subtype.val (_ : HermitianMat _ _)] -meta def evalHermitianMatVal : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatVal : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do /- Note: we must not call `whnf` on `e` because `Subtype.val` is a structure projection (reducible), so `whnf` would reduce it and destroy the pattern. -/ let A := e.appArg! @@ -606,14 +615,16 @@ meta def evalHermitianMatVal : PositivityExt where eval {_u _α} _zα _pα e := /-- Positivity extension for `M * Mᴴ` as a Matrix: always nonneg. -/ @[positivity HMul.hMul _ (Matrix.conjTranspose _)] -meta def evalMatrixSelfMulConjTranspose : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalMatrixSelfMulConjTranspose : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app (.app _hmul _M) Mstar ← whnfR e | throwError "not HMul application" let .app _conjTranspose M' ← whnfR Mstar | throwError "not M * conjTranspose" pure (.nonnegative (← mkAppM ``Matrix.nonneg_self_mul_conjTranspose #[M'])) /-- Positivity extension for `Mᴴ * M` as a Matrix: always nonneg. -/ @[positivity HMul.hMul (Matrix.conjTranspose _) _] -meta def evalMatrixConjTransposeMulSelf : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalMatrixConjTransposeMulSelf : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app (.app _hmul Mstar) _M ← whnfR e | throwError "not HMul application" let .app _conjTranspose M' ← whnfR Mstar | throwError "not conjTranspose * M" pure (.nonnegative (← mkAppM ``Matrix.nonneg_conjTranspose_mul_self #[M'])) @@ -621,7 +632,8 @@ meta def evalMatrixConjTransposeMulSelf : PositivityExt where eval {_u _α} _zα /-- Positivity extension for `⟨M, (pf : M.IsHermitian)⟩` as a HermitianMat: equivalent to `0 ≤ M` in `MatrixOrder`. -/ @[positivity (Subtype.mk _ _ : HermitianMat _ _)] -meta def evalHermitianMatMk : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatMk : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app (.app _mkFn val) _proof ← whnfR e | throwError "not Subtype.mk" match ← bestResult val with | (true, pa) => @@ -633,7 +645,8 @@ meta def evalHermitianMatMk : PositivityExt where eval {_u _α} _zα _pα e := d Will try to prove `0 ≤ M` in the `MatrixOrder`. If the proof is `A.H`, i.e. M comes from a HermitianMat, this will give `0 ≤ A.mat` which becomes `0 ≤ A` later. -/ @[positivity Matrix.IsHermitian.eigenvalues _ _] -meta def evalMatrixEigenvalues : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalMatrixEigenvalues : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app (.app _eigenvaluesFn hProof) _i ← whnfR e | throwError "not eigenvalues application" let pType ← inferType hProof if pType.isAppOf ``Matrix.IsHermitian then diff --git a/QuantumInfo/ForMathlib/HermitianMat/Proj.lean b/QuantumInfo/ForMathlib/HermitianMat/Proj.lean index 486d825c3..46c32c3e0 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Proj.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Proj.lean @@ -193,7 +193,7 @@ lemma projector_support_eq_sum : A.supportProj.mat = simp_all [ Finset.sum_ite ]; convert h_sum_rankOne using 1; · exact h_support ▸ rfl; - · refine' Finset.sum_bij ( fun i hi => ⟨ i, by simpa using hi ⟩ ) _ _ _ _ <;> simp [ Finset.mem_filter ] + · refine' Finset.sum_bij ( fun i hi => ⟨ i, by simpa using hi ⟩ ) _ _ _ _ <;> simp [ Finset.mem_filter, hb ] /- `HermitianMat.supportProj` as a cfc. diff --git a/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean b/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean index 5a7a5236f..4eb8660a1 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Schatten.lean @@ -40,7 +40,7 @@ theorem schattenNorm_hermitian_pow {A : HermitianMat d ℂ} (hA : 0 ≤ A) {p : simp only [HermitianMat.conjTranspose_mat, HermitianMat.mat_pow] convert rfl using 2 rw [sq] - exact Matrix.IsHermitian.cfc_eq _ _ + exact congrFun (congrFun (Matrix.IsHermitian.cfc_eq _ _) _) _ lemma schattenNorm_nonneg (A : Matrix d d ℂ) (p : ℝ) : 0 ≤ schattenNorm A p := by diff --git a/QuantumInfo/ForMathlib/HermitianMat/Sqrt.lean b/QuantumInfo/ForMathlib/HermitianMat/Sqrt.lean index 858d572df..1804aeee8 100644 --- a/QuantumInfo/ForMathlib/HermitianMat/Sqrt.lean +++ b/QuantumInfo/ForMathlib/HermitianMat/Sqrt.lean @@ -74,7 +74,8 @@ theorem sqrt_posDef {A : HermitianMat d 𝕜} (hA : A.mat.PosDef) : open Lean Meta Mathlib.Meta.Positivity in /-- Positivity extension for `HermitianMat.sqrt` -/ @[positivity HermitianMat.sqrt _] -meta def evalHermitianMatSqrt : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalHermitianMatSqrt : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let .app _sqrt (A : Expr) ← whnfR e | throwError "not sqrt application" try let (isStrictA, pfA) ← bestResult A diff --git a/QuantumInfo/ForMathlib/SionMinimax.lean b/QuantumInfo/ForMathlib/SionMinimax.lean index c6e379814..e2aaaeed5 100644 --- a/QuantumInfo/ForMathlib/SionMinimax.lean +++ b/QuantumInfo/ForMathlib/SionMinimax.lean @@ -263,23 +263,30 @@ theorem LeftOrdContinuous.comp_lowerSemicontinuousOn_strong_assumptions {α γ LowerSemicontinuousOn (g ∘ f) s := by intros x hx y hy have hU : ∃ U ∈ nhds x, ∀ z ∈ U ∩ s, g (f z) > y := by - simp_all only [Set.mem_inter_iff, gt_iff_lt, and_imp] - obtain ⟨z, hz1, hz2⟩ : ∃ z, y < g z ∧ z < f x := by - obtain ⟨z, hz⟩ : ∃ z, z < f x ∧ y < g z := by - by_contra h_contra - simp only [not_exists, not_and, not_lt] at h_contra - have h_exists_z : ∃ z, z < f x ∧ g z > y := by - have h_lub : IsLUB (Set.Iio (f x)) (f x) := by - exact isLUB_Iio - have := hg h_lub; - have := this.exists_between hy - simp_all only [Set.mem_image, Set.mem_Iio, exists_exists_and_eq_and, gt_iff_lt] - grind - exact h_exists_z.choose_spec.2.not_ge ( h_contra _ h_exists_z.choose_spec.1 ); - aesop - specialize hf x hx z hz2 - rw [ eventually_nhdsWithin_iff ] at hf - exact ⟨_, hf, fun _ hx hx' ↦ hz1.trans_le (hg2 (hx hx').le)⟩ + by_cases hne : (Set.Iio (f x)).Nonempty + · simp_all only [Set.mem_inter_iff, gt_iff_lt, and_imp] + obtain ⟨z, hz1, hz2⟩ : ∃ z, y < g z ∧ z < f x := by + obtain ⟨z, hz⟩ : ∃ z, z < f x ∧ y < g z := by + by_contra h_contra + simp only [not_exists, not_and, not_lt] at h_contra + have h_exists_z : ∃ z, z < f x ∧ g z > y := by + have h_lub : IsLUB (Set.Iio (f x)) (f x) := by + exact isLUB_Iio + have := hg hne h_lub + have := this.exists_between hy + simp_all only [Set.mem_image, Set.mem_Iio, exists_exists_and_eq_and, gt_iff_lt] + grind + exact h_exists_z.choose_spec.2.not_ge ( h_contra _ h_exists_z.choose_spec.1 ) + aesop + specialize hf x hx z hz2 + rw [ eventually_nhdsWithin_iff ] at hf + exact ⟨_, hf, fun _ hx hx' ↦ hz1.trans_le (hg2 (hx hx').le)⟩ + · refine ⟨Set.univ, Filter.univ_mem, fun z _ ↦ ?_⟩ + rw [Set.not_nonempty_iff_eq_empty] at hne + have hmin : f x ≤ f z := by + by_contra h + exact Set.eq_empty_iff_forall_notMem.mp hne (f z) (not_le.mp h) + exact lt_of_lt_of_le hy (hg2 hmin) simp only [Set.mem_inter_iff, and_imp] at hU obtain ⟨w, ⟨left, right⟩⟩ := hU exact Filter.eventually_inf_principal.2 (Filter.mem_of_superset left right) @@ -665,7 +672,6 @@ private lemma sion_exists_min_fin ext simp [S'] rw [hS'_compl] at hS_diff_ne ⊢ - rw [Set.coe_setOf] at hS_diff_ne refine hab.trans_le ?_ simp apply le_ciInf diff --git a/QuantumInfo/States/Mixed/MState.lean b/QuantumInfo/States/Mixed/MState.lean index 12446857d..2d9b5e7a4 100644 --- a/QuantumInfo/States/Mixed/MState.lean +++ b/QuantumInfo/States/Mixed/MState.lean @@ -97,7 +97,8 @@ open Lean Meta Mathlib.Meta.Positivity in Note: we must not call `whnfR` on `e` because `MState.M` is a structure projection (reducible), so `whnfR` would reduce it and destroy the pattern. -/ @[positivity MState.M _] -meta def evalMStateM : PositivityExt where eval {_u _α} _zα _pα e := do +meta def evalMStateM : PositivityExt where eval {_u _α} _zα _pα? e := + match _pα? with | none => pure .none | some _ => do let ρ := e.appArg! pure (.positive (← mkAppM ``MState.pos #[ρ])) @@ -152,9 +153,9 @@ instance instMixable : Mixable (HermitianMat d ℂ) (MState d) where h.casesOn fun t ht ↦ ht ▸ t.tr⟩, rfl⟩ convex := convex d +include ρ in /-- An MState is a witness that d is nonempty. -/ -@[implicit_reducible] -def nonempty : Nonempty d := by +lemma nonempty : Nonempty d := by by_contra h simpa [HermitianMat.trace_eq_re_trace, not_nonempty_iff.mp h] using ρ.tr @@ -1157,7 +1158,7 @@ lemma multiset_spectrum_relabel_eq {d₁ d₂ : Type*} [Fintype d₁] [Decidable congr! 2; exact beq_eq_beq.mp rfl -def spectrum_SWAP (ρ : MState (d₁ × d₂)) : ∃ e, ρ.SWAP.spectrum.relabel e = ρ.spectrum := by +lemma spectrum_SWAP (ρ : MState (d₁ × d₂)) : ∃ e, ρ.SWAP.spectrum.relabel e = ρ.spectrum := by -- Apply the lemma exists_equiv_of_multiset_map_eq with the appropriate parameters. obtain ⟨w, h⟩ := exists_equiv_of_multiset_map_eq (fun p => ρ.spectrum p) (fun p => ρ.SWAP.spectrum p) (ρ.multiset_spectrum_relabel_eq (Equiv.prodComm _ _).symm ▸ rfl) diff --git a/QuantumInfo/States/Pure/Braket.lean b/QuantumInfo/States/Pure/Braket.lean index e23c1e2a3..99141fc87 100644 --- a/QuantumInfo/States/Pure/Braket.lean +++ b/QuantumInfo/States/Pure/Braket.lean @@ -193,7 +193,7 @@ def Bra.normalize (v : d → ℂ) (h : ∃ x, v x ≠ 0) : Bra d := } /-- A bra is already normalized -/ -def Bra.normalize_ket_eq_self (ψ : Bra d) : Bra.normalize (ψ.vec) (Bra.exists_ne_zero ψ) = ψ := by +lemma Bra.normalize_ket_eq_self (ψ : Bra d) : Bra.normalize (ψ.vec) (Bra.exists_ne_zero ψ) = ψ := by ext x unfold normalize simp only [apply, ψ.normalized', Real.sqrt_one, Complex.ofReal_one, div_one] diff --git a/README.md b/README.md index d9cd9fa29..7827ff7a8 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ [![](https://img.shields.io/badge/View_The-Stats-blue)](https://physlib.io/Stats) -[![](https://img.shields.io/badge/Lean-v4.31.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.31.0) +[![](https://img.shields.io/badge/Lean-v4.32.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.32.0) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/physlib) [![Ask DeepWiki](https://deepwiki.com/badge.svg)](https://deepwiki.com/leanprover-community/physlib) [![api_docs](https://img.shields.io/badge/doc-API_docs-blue)](https://physlib.io/docs/) diff --git a/lake-manifest.json b/lake-manifest.json index 8e3dcf43e..de4da1837 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", + "rev": "81a5d257c8e410db227a6665ed08f64fea08e997", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "0bc516c1b9db83658d6475c40d9b1ed71219b921", + "rev": "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", + "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", + "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", + "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", + "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fa08db58b30eb033edcdab331bba000827f9f785", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0be4df908d1a8e75b58961041e2b4973692623df", + "rev": "b2e8105c3507d81adaa531fda5990d14b631528f", "name": "leansqlite", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,17 +105,17 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", + "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", + "inputRev": "v4.32.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "a2e430a4c9d3ad24078b8581fe0162fc5b0c9a6c", + "rev": "947120c17904da8fc89abe3616d57e1c3e13aa9c", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,17 +125,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "rev": "b648facb6be09a29be636bbc02d28ddee77565c7", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 718bae2f1..7c6bb1196 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,12 +4,12 @@ defaultTargets = ["Physlib", "QuantumInfo"] [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "v4.31.0" +rev = "v4.32.0" [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.31.0" +rev = "v4.32.0" [[lean_lib]] name = "Physlib" diff --git a/lean-toolchain b/lean-toolchain index 133a3f7d6..2544c30c5 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 \ No newline at end of file +leanprover/lean4:v4.32.0 \ No newline at end of file From ad6a2a1d90af6d8babb02660ad4253fe945b8bfa Mon Sep 17 00:00:00 2001 From: Alex-Zughaid <117576511+Alex-Zughaid@users.noreply.github.com> Date: Tue, 21 Jul 2026 12:54:00 +0100 Subject: [PATCH 2/2] random change made by claude - just to test the PR --- .../FluidDynamics/NavierStokes/Momentum.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Physlib/FluidDynamics/NavierStokes/Momentum.lean b/Physlib/FluidDynamics/NavierStokes/Momentum.lean index 40928d4fd..bc2c8d4f4 100644 --- a/Physlib/FluidDynamics/NavierStokes/Momentum.lean +++ b/Physlib/FluidDynamics/NavierStokes/Momentum.lean @@ -251,5 +251,23 @@ theorem momentumEquation_iff_convectiveMomentumEquation exact ⟨fun h t x => (conservative_eq_convective_lhs t x).symm.trans (h t x), fun h t x => (conservative_eq_convective_lhs t x).trans (h t x)⟩ +/-! + +## E. Basic properties of momentum fields + +-/ + +/-- The momentum density vanishes wherever the mass density is zero. -/ +lemma momentumDensity_zero_of_rho_zero (d : ℕ) (fluid : FluidState d) + (t : Time) (x : Space d) (h : fluid.rho t x = 0) : + momentumDensity d fluid t x = 0 := by + simp [momentumDensity, h] + +/-- The momentum flux vanishes wherever the mass density is zero. -/ +lemma momentumFlux_zero_of_rho_zero (d : ℕ) (fluid : FluidState d) + (t : Time) (x : Space d) (h : fluid.rho t x = 0) : + momentumFlux d fluid t x = 0 := by + simp [momentumFlux, h] + end NavierStokes end FluidDynamics