weakFieldAlgebraStub

formal source

 100
 101instance : FieldTheoryFacts := fieldTheoryStub
 102
 103noncomputable def weakFieldAlgebraStub : WeakFieldAlgebraFacts where
 104  inverse_first_order_identity_minkowski := by
 105    intro h x μ ν
 106    have : |(0 : ℝ)| ≤ 8 * h.eps + 4 * h.eps ^ 2 := by
 107      have hnonneg : 0 ≤ 8 * h.eps + 4 * h.eps ^ 2 := by
 108        have := le_of_lt h.eps_pos
 109        nlinarith [this]
 110      simpa using hnonneg
 111    simpa using this
 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