Merged
Conversation
* feat: Update EM results * refactor: Restructuring EM files * refactor: Lint * refactor: Lint * feat: Add speed of light and other constants to EM * feat: Update boosts of electric & magnetic field * feat: Update constant fields * refactor: fix build * refactor: Lint * refactor: Main docs * reactor: Fix Lint
* refactor: Add changes * refactor: Fix build * refactor: docs and lint * refactor: free simps
* feat: Add Lorentz action on distributions * refactor: Lint * refactor: Update docs * Update PhysLean.lean
* feat: Add Plane waves * feat: Remove unused files * refactor: Lint * refactor: Add documentation
* feat: Add Plane waves * feat: Remove unused files * refactor: Lint * refactor: Add documentation * feat: Add space time integrals * refactor: Fix build * refactor: Lint
* refactor: Add Radial Angular Measure * Update RadialAngularMeasure.lean
* feat: Refactor ofFunction and add time integrals * refactor: Lint * refactor: Fix warning
* feat: Add norm properties on space * refactor: Lint
* feat: Add more properties of the norm * refactor: LInt
* Fill in sorry for solidSphere_centerOfMass * Use norm_num instead of simp
Co-authored-by: Aristotle Harmonic [aristotle-harmonic@harmonic.fun](mailto:aristotle-harmonic@harmonic.fun). Co-Authored-By: Aristotle <232223898+aristotle-harmonic@users.noreply.github.com>
* fix: Trying to address GHI 808 * Improving example * Removing checks * fix: Changing from := to where definition * fix: Adding and fixing additional example * Adding example for Q.eigenfunction 0 * Moving File * Adding the new example file as import * Minor Cleanup * Removing double empty line (linting) * fix: Fixing order of imports * fix: In PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Examples.lean fixing namespaces
* feat: Create slices for Space Lots of things about distributions here, which may best be seperated. * refactor: Linting * docs: Add documentation * refactor: Lint
* feat: Update ConstantTimeDist dimensions * refactor: Golfing
* feat: Update verisons * feat: Fix build, pass 1 * fix: Build pass 2 * feat: fix build pass 3 * feat: Fix build * refactor: style Lint * refactor: Lint * refactor: Lint * fix: Build
* feat: Add DistElectromagneticPotential, basic properties * refactor: Lint * refactor: LInt
…816) * feat: Improvements to the API around EM potentials as distributions * refactor: Update one dimension point particle * refactor: LInt * refactor: Lint
…ory docstring (#817) * Add files via upload * line lengths made less than 100 * made line length less than 100 characters Clarified problem statement and solution steps for the Coplanar Double Pendulum, improving readability and structure. * made line length less than 100 * Fix formatting * line width made 100 Refined the problem statement and solution for the coplanar double pendulum, improving clarity and correcting formatting issues. * made all comments less than 100 lines * Add imports for double and sliding pendulum modules * Add copyright and license details Added copyright and licensing information to the file. * Add copyright and license details to the file Added copyright and licensing information. * Delete PhysLean/ClassicalMechanics/Pendulum/Coplanar_Double_Pendulum.lean * Delete PhysLean/ClassicalMechanics/Pendulum/Miscellaneous_Pendulum_Pivot_motions.lean * Delete PhysLean/ClassicalMechanics/Pendulum/Sliding_Pendulum.lean * Add files via upload * Refactor import statements for pendulum modules
* feat: Start refactoring Space * feat: fix builds * feat: Fix build * refactor: Lint * refactor: Remove SpaceStruct * refactor: Remove transitive import
* FA: Reset the entire repo to upstream, created a new branch for the first proof (ideal gas adiabats), then re-added the file for the proof of the aidabats in the ideal gas * FA: edited IdealGas/Basic.lean to pass the linter ./scripts/lint-style.sh * FA: cleaned up the IdealGas/Basic.lean file to pass linters. Removed transitive imports, unused code, and added documentation * FA: edited doc string
* Added latex equation for pendulum files * removed pendulum files * removed pendulum files * corrected coplanar pendulum file
* feat: Start refactoring Space * feat: fix builds * feat: Fix build * refactor: Lint * refactor: Remove SpaceStruct * refactor: Remove transitive import * feat: Add Kinetic Term for Distributions * Update Basic.lean * refactor: Lint and add infinite wire * refactor: Documentation * refactor: Documentation * docs: Add documentation * refactor: Lint * refactor: Add file for ciruclar coil * refactor: Lint
* feat: invariance of the speed of light * refactor: Lint
* feat: Prove the equivariance of the field strength * refactor: Lint
chore: remove Cyrillic docstring
chore: remove sorries in 4.27.0
Co-authored-by: kastch <kastch>
* Remove sorry: Prove realLorentzTensor.prodT_toComplex * Added comments/file organization for realLorentzTenzor * Added sections according to table of contents for realLorentzTenzor --------- Co-authored-by: kastch <kastch>
* Clarify steps for bumping dependencies in Bump.yml Updated instructions for removing the .lake file and running lake update. * Update label for previous bumps in issue template * Update references to HEPLean
* feat: add results about specific 2HDM potential * refactor: fix lint
Co-authored-by: kastch <kastch>
* Remove sorry: prove realLorentzTensor.evalT_toComplex * Linter fixes in realLorentzTensor.evalT_toComplex --------- Co-authored-by: kastch <kastch>
* refactor: positionOperator * feat: (regularized) radius operator * feat: (regularized) LRL vector * feat: radius op commutators * feat: commute * minor changes * feat: LRL vector, commutators and square * golf + removing "simp only"s * minor clean-up * improved comments * [H,A] sorry free * rpow name change * linter fixes * linter fixes v2 * naming improvements * todo: normRegularizedPow
* feat: Started working on GHI 846 * Fixing Linter * Fix * Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix Lean Style * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Fix * fix: Copyright Fix * fix: Fixing Author
refactor: remove a few `erw`s
chore: remove unused simp lemmas
* feat: 2HDM clean up * feat: Add enough little lemma * feat: Another small lemma * refactor: review changes
chore: bump to v4.28.0
feat(Basic): prove `linSolsIncl_injective`
Co-authored-by: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
feat(Generalized): prove `generalizedBoost_timeComponent_eq`
* d-dim Hilbert space * d-dim schwartz submodule * init progress on unbounded ops * init progress on unbounded ops * submodule lemmas * abstract away Hilbert space * linter fixes * sorry removed: closable => adjoint dense * sorry removed: symm + dense => closable * sorry-free * comments * UnboundedOperator extends LinearPMap * remove unnecessary coe * relocate submodule lemmas * style improvements * more improvements * extract adjoint_isClosable_dense * minor cleanup * lint fixes * Remove extra blank lines * Remove extra blank lines --------- Co-authored-by: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
20 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.