feat(FluidDynamics): add pressure field API#1272
Conversation
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
|
closing this as I believe @FloWsnr approach already has this covered properly |
This adds a small pressure-field layer to
FluidDynamics, built on the existingFluidState, stress-tensor, and momentum-balance API. It is meant as a starting point for the pressure API discussed in #862; I kept it to the parts the current library supports cleanly, and can adjust the shape to fit the intended requirements.Added
Physlib/FluidDynamics/Pressure.lean:PressureField: a scalar pressure field.FluidWithPressure: aFluidStatetogether with a pressure field.pressureStress: the isotropic pressure stress-p • I;pressureStress_apply,pressureStress_offDiag, andpressureStress_symmgive its components and symmetry.pressureForce: the pressure force density-∇p, withpressureForce_apply.matrixDiv_pressureStress: the divergence of the pressure stress equals the pressure force, the bridge into the momentum balance.toMomentumBalance: packages aFluidWithPressureas momentum-balance data.Physlib.lean: imports the new module.Reviewer map
Pressure.leanreads top to bottom: the field andFluidWithPressure, then the stress tensor and its lemmas, then the force and thematrixDiv_pressureStressbridge, and finallytoMomentumBalance.