module
module
IndisputableMonolith.Masses.GapFunctionForcing
show as:
view Lean formalization →
depends on (2)
declarations in this module (14)
-
def
gapAffineLogR -
def
gapAffineLog -
lemma
phi_eq_one_add_inv_phi -
lemma
one_add_inv_phi_eq_phi -
lemma
log_one_add_inv_phi_eq_log_phi -
lemma
zero_normalization_forces_offset -
lemma
unit_step_forces_log_scale -
lemma
minus_one_step_forces_phi_shift -
theorem
affine_log_parameters_forced_by_three_point_calibration -
theorem
affine_log_collapses_to_canonical_gap -
theorem
affine_log_collapses_from_three_point_calibration -
theorem
affine_log_unique_under_normalizations -
structure
ThreePointAffineLogClosure -
theorem
three_point_affine_log_closure