phiPsiCouplingStub

formal source

 112
 113instance : WeakFieldAlgebraFacts := weakFieldAlgebraStub
 114
 115noncomputable def phiPsiCouplingStub : PhiPsiCouplingFacts where
 116  phi_minus_psi_difference := by
 117    intro ng α C_lag x
 118    refine ⟨0, ?_, ?_⟩
 119    · simp
 120    · norm_num
 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