module
module
IndisputableMonolith.QFT.CasimirPhiCorrections
show as:
view Lean formalization →
used by (2)
depends on (1)
declarations in this module (14)
-
inductive
MaterialBoundary -
inductive
CasimirGeometry -
structure
PhiCorrectionInputs -
structure
PhiCorrectionModel -
def
correctedPressure -
theorem
correctedPressure_eq_ideal_of_delta_zero -
theorem
correctedPressure_more_attractive_of_delta_pos -
theorem
correctedPressure_negative_of_delta_gt_neg_one -
theorem
correctedPressure_repulsive_of_delta_lt_neg_one -
structure
MaterialPhiHypothesis -
structure
MaterialCeilingHypothesis -
theorem
correctedPressure_negative_under_material_ceiling -
structure
PhiCorrectionCert -
def
phiCorrectionCert