-- Generated by scripts/vii24r/publish/gen_platform_tree_unitA.py (Atlas VII Unit A; copy of the RELEASE06 generator, header only) by skeleton subtraction from Atlas/EinsteinMaxwell/ES5/KerrSchild/PaperGauge.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.Afun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.Dfun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.Ffun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.Gfun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.Hfun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.Kfun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.PaperData, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.eFun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.ellFun, ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial.qFun
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_D_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Defs
import Definitions.Def_Atlas_EinsteinMaxwell_ES5_Generic_Data

/-! # VII-02 (F2a): paper-gauge dictionary for the VI equal-spin radial functions

Real functions `f, m, N, w, p, a` of the VI radial variable `R` (the paper's squared radius;
no areal-coordinate change is made). On an open set `I` they are `C^∞` and `f, m, N` vanish
nowhere (`PaperData`, regularity and non-vanishing only — no field equation, no conservation
law, no sign). The dictionary to the VI data `ESData I B D A H W Φ Ψ` is

  `B = f, D = m/(4 f N), A = m/f, H = N/m, W = w, Φ = p, Ψ = a`,

and the derived functions are `e = p' + w a'`, `F = f/N`, `q = (N/f) e`, `K = N²/(f m)`,
`ℓ = K w' - 4 q a`, `G = a' p'' - p' a''`. All derivative lemmas below are genuine `HasDerivAt`
statements at points of `I`, obtained from `hasDerivAt_of_cd` / `cd_deriv` and the product,
quotient and power rules. -/

open scoped ContDiff
open ExactVacuumAtlas.EinsteinMaxwell.ES5

namespace ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial

/-- `D = m / (4 f N)`. -/
noncomputable def Dfun (f m N : ℝ → ℝ) : ℝ → ℝ := fun r => m r / (4 * f r * N r)
/-- `A = m / f`. -/
noncomputable def Afun (f m : ℝ → ℝ) : ℝ → ℝ := fun r => m r / f r
/-- `H = N / m`. -/
noncomputable def Hfun (m N : ℝ → ℝ) : ℝ → ℝ := fun r => N r / m r

/-- Paper-gauge radial data: `C^∞` on the open set `I`, and `f, m, N` nowhere zero on `I`. -/
structure PaperData (I : Set ℝ) (f m N w p a : ℝ → ℝ) : Prop where
  isOpen : IsOpen I
  cf : ContDiffOn ℝ ∞ f I
  cm : ContDiffOn ℝ ∞ m I
  cN : ContDiffOn ℝ ∞ N I
  cw : ContDiffOn ℝ ∞ w I
  cp : ContDiffOn ℝ ∞ p I
  ca : ContDiffOn ℝ ∞ a I
  nf : ∀ r ∈ I, f r ≠ 0
  nm : ∀ r ∈ I, m r ≠ 0
  nN : ∀ r ∈ I, N r ≠ 0

/-- `e = p' + w a'`. -/
noncomputable def eFun (w p a : ℝ → ℝ) : ℝ → ℝ := fun r => deriv p r + w r * deriv a r
/-- `F = f / N`. -/
noncomputable def Ffun (f N : ℝ → ℝ) : ℝ → ℝ := fun r => f r / N r
/-- `q = (N / f) e`. -/
noncomputable def qFun (f N w p a : ℝ → ℝ) : ℝ → ℝ := fun r => N r / f r * eFun w p a r
/-- `K = N² / (f m)`. -/
noncomputable def Kfun (f m N : ℝ → ℝ) : ℝ → ℝ := fun r => N r ^ 2 / (f r * m r)
/-- `ℓ = K w' - 4 q a`. -/
noncomputable def ellFun (f m N w p a : ℝ → ℝ) : ℝ → ℝ :=
  fun r => Kfun f m N r * deriv w r - 4 * qFun f N w p a r * a r
/-- The real geodesic defect `G = a' p'' - p' a''`. -/
noncomputable def Gfun (p a : ℝ → ℝ) : ℝ → ℝ :=
  fun r => deriv a r * deriv (deriv p) r - deriv p r * deriv (deriv a) r

variable {I : Set ℝ} {f m N w p a : ℝ → ℝ} {r : ℝ}

namespace PaperData

end PaperData

/-! ## Genuine derivatives of the dictionary and derived functions at points of `I` -/

end ExactVacuumAtlas.EinsteinMaxwell.ES5.KerrSchild.Radial