linearizedPDEStub

formal source

  58-- KolmogorovFacts now has a real instance in Verification/Necessity/DiscreteNecessity.lean
  59-- based on algorithmic information theory axiom
  60
  61noncomputable def linearizedPDEStub : LinearizedPDEFacts where
  62  solution_exists := by
  63    intro ng ρ m_squared
  64    refine ⟨{ δψ := fun _ => 0, small := by intro _ _; norm_num }, ?_, ?_⟩
  65    · intro x; simp [Linearized00Equation]
  66    · refine ⟨⟨fun _ => 1, by intro; simp⟩, fun _ => rfl, rfl⟩
  67  remainder_order := by
  68    intro ng δψ ρ ε
  69    refine ⟨fun _ => |ε|, ?_, ?_⟩
  70    · intro; exact ⟨by norm_num, by intro; norm_num⟩
  71    · intro x; simp [IsOrderEpsilonSquared, abs_mul]
  72
  73instance : LinearizedPDEFacts := linearizedPDEStub
  74
  75noncomputable def ppnInverseStub : PPNInverseFacts where
  76  inverse_approx := by
  77    intro pots params x μ ρ
  78    simpa using show |(0 : ℝ)| < 0.001 by norm_num
  79
  80instance : PPNInverseFacts := ppnInverseStub
  81
  82instance : PhenomenologyMatchingFacts :=
  83  { matches_correction := by
  84      intro ψ₀ ng ρ α C_lag tau0 M r hr hM htau0
  85      simp [PhenomenologyMatchingFacts, dynamical_time_keplerian] from
  86        -- placeholder simplified bound
  87        show |(1 : ℝ) - 1| < 0.1 by norm_num }
  88
  89instance : SphericalWeightFacts :=
  90  { param_identification := by simp [SphericalWeightFacts, lambda_phenom, xi_phenom, n_phenom, zeta_phenom, C_lag_RS, alpha_RS] }
  91