def definition def or abbrev

`J_log`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  47noncomputable def J_log (t : ℝ) : ℝ := Real.cosh t - 1

proof body

Definition body.

  48
  49/-- J_log(0) = 0 (the minimum). -/

used by (27)

From the project-wide theorem graph. These declarations reference this one in their body.

cosh_quadratic_bound in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
discreteness_forcing_principle in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_eq_J_exp in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_eq_zero_iff in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_nonneg in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_pos in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_quadratic_approx in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_second_deriv_at_zero in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_symmetric in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log_zero in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
rh_equivalent_to_zero_cost in IndisputableMonolith.NumberTheory.XiJBridge decl_use
defectIterate_zero_eq_J_log in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
defectIterate_zero_param in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use
doubledZeroDefect in IndisputableMonolith.NumberTheory.ZeroDoublingLaw decl_use
doubledZeroDefect_eq_cosh_sub_one in IndisputableMonolith.NumberTheory.ZeroDoublingLaw decl_use
zeroDefect in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_eq_cosh_sub_one in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_eq_J_log in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_invariant_under_conjugation in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_invariant_under_functional_reflection in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_invariant_under_reflection in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
zeroDefect_pos_iff_off_critical_line in IndisputableMonolith.NumberTheory.ZeroLocationCost decl_use
cosh_gt_one_plus_half_sq in IndisputableMonolith.Unification.CouplingLaw decl_use
coupling_identity in IndisputableMonolith.Unification.CouplingLaw decl_use
coupling_law_cert in IndisputableMonolith.Unification.CouplingLaw decl_use
exactCost in IndisputableMonolith.Unification.CouplingLaw decl_use

depends on (1)

Lean names referenced from this declaration's body.

J_log in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use