`G`

definition

show as: view math explainer →

module: IndisputableMonolith.Cost.FunctionalEquation
domain: Cost
line: 23 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.FunctionalEquation on GitHub at line 23.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  20open Real
  21
  22/-- Log-coordinate reparametrization: `G_F t = F (exp t)` -/
  23@[simp] noncomputable def G (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)
  24
  25/-- Convenience reparametrization: `H_F t = G_F t + 1`. -/
  26@[simp] noncomputable def H (F : ℝ → ℝ) (t : ℝ) : ℝ := G F t + 1
  27
  28/-- The cosh-type functional identity for `G_F`. -/
  29def CoshAddIdentity (F : ℝ → ℝ) : Prop :=
  30  ∀ t u : ℝ,
  31    G F (t+u) + G F (t-u) = 2 * (G F t * G F u) + 2 * (G F t + G F u)
  32
  33/-- Direct cosh-add identity on a function. -/
  34def DirectCoshAdd (Gf : ℝ → ℝ) : Prop :=
  35  ∀ t u : ℝ,
  36    Gf (t+u) + Gf (t-u) = 2 * (Gf t * Gf u) + 2 * (Gf t + Gf u)
  37
  38lemma CoshAddIdentity_implies_DirectCoshAdd (F : ℝ → ℝ)
  39  (h : CoshAddIdentity F) :
  40  DirectCoshAdd (G F) := h
  41
  42lemma G_even_of_reciprocal_symmetry
  43  (F : ℝ → ℝ)
  44  (hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹) :
  45  Function.Even (G F) := by
  46  intro t
  47  have hpos : 0 < Real.exp t := Real.exp_pos t
  48  have hrec : Real.exp (-t) = (Real.exp t)⁻¹ := by simp [Real.exp_neg]
  49  simp [G, hrec, hSymm hpos]
  50
  51lemma G_zero_of_unit (F : ℝ → ℝ) (hUnit : F 1 = 0) : G F 0 = 0 := by
  52  simpa [G] using hUnit
  53

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.