Existence.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SepticProfile.exists_global_phase_input line 14
Source documentation
A positive smooth radial phase with timelike gradient and vanishing phase transport, together with its positive septic amplitude, in four spatial dimensions.
```
theorem exists_global_phase_input :
    ∃ P : GlobalProfile,
      (∀ y : ℝ, 0<P.H y) ∧
      (∃ Hrad : ℝ → ℝ, ContDiffOn ℝ ∞ Hrad (Ici 0) ∧
        ∀ y : ℝ, P.H y=Hrad (y^2)) ∧
      (∀ t : ℝ, 0<t → ∀ X : PhysicalSpace,
        0 < minkowskiSquare P.s0 t X ∧ phaseTransport P.s0 t X=0 ∧
        0<P.w0 t X) := by
…
```
Mentions: OAI.SepticProfile.GlobalProfile, OAI.SepticProfile.PhysicalSpace, OAI.SepticProfile.minkowskiSquare, OAI.SepticProfile.phaseTransport