modifiedPoissonStub

formal source

 121
 122instance : PhiPsiCouplingFacts := phiPsiCouplingStub
 123
 124noncomputable def modifiedPoissonStub : ModifiedPoissonPDEFacts where
 125  poisson_solution_unique := by
 126    intro ρ w Φ₁ Φ₂ h₁ h₂ r hr
 127    exact ⟨0, rfl⟩
 128  fundamental_modified_poisson := by
 129    intro ψ₀ ng ρ α C_lag x
 130    simp
 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