def
definition
radialPoissonStub
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.NewFixtures on GitHub at line 134.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
131
132instance : ModifiedPoissonPDEFacts := modifiedPoissonStub
133
134noncomputable def radialPoissonStub : RadialPoissonFacts where
135 laplacian_spherical := by
136 intro f r
137 simp
138 radial_poisson_solution_exists := by
139 intro rho w
140 exact ⟨fun _ => 0, by intro r hr; simp [RadialPoissonPhi]⟩
141
142instance : RadialPoissonFacts := radialPoissonStub
143
144noncomputable def christoffelStub : ChristoffelExpansionFacts where
145 christoffel_expansion_minkowski := by
146 intro hWF x ρ μ ν
147 have : |(0 : ℝ)| ≤ 40 * hWF.eps ^ 2 := by
148 have hnonneg : 0 ≤ 40 * hWF.eps ^ 2 := by
149 have := sq_nonneg hWF.eps
150 nlinarith
151 simpa using hnonneg
152 simpa using this
153 newtonian_00_formula := by
154 intro ng x
155 simp [ChristoffelExpansionFacts]
156
157instance : ChristoffelExpansionFacts := christoffelStub
158
159noncomputable def coneEntropyStub : ConeEntropyFacts where
160 cone_entropy_bound := by
161 intro α cone area
162 simp
163
164instance : ConeEntropyFacts := coneEntropyStub