OAI/Analysis/CoulombTransport/LocalImplicit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.LocalImplicit.exists_analytic_implicit_branch line 20

   Source documentation

   Analytic implicit-function theorem, packaged on open product neighborhoods. The equation is normalized to zero, as for a stationary-point equation.

   theorem exists_analytic_implicit_branch
       (G : P × S → S) (p : P) (s : S)
       (hG : ContDiffAt ℝ ω G (p, s))
       (hzero : G (p, s) = 0)
       (hinv : (fderiv ℝ G (p, s) ∘L ContinuousLinearMap.inr ℝ P S).IsInvertible) :
       ∃ (ψ : P → S) (U : Set P) (V : Set S),
         IsOpen U ∧ p ∈ U ∧ IsOpen V ∧ s ∈ V ∧
         ContDiffOn ℝ ω ψ U ∧ MapsTo ψ U V ∧ ψ p = s ∧
         (∀ y ∈ U, G (y, ψ y) = 0) ∧
         (∀ y ∈ U, ∀ z ∈ V, G (y, z) = 0 ↔ ψ y = z) ∧
         HasStrictFDerivAt ψ
           (-(fderiv ℝ G (p, s) ∘L ContinuousLinearMap.inr ℝ P S).inverse ∘L
   …

2. theorem OAI.Problem356.LocalImplicit.exists_analytic_local_diffeomorph line 59

   Source documentation

   A map analytic at one point with invertible derivative is analytic in both directions on a suitable open partial homeomorphism.

   theorem exists_analytic_local_diffeomorph
       (f : P → S) (p : P)
       (hf : ContDiffAt ℝ ω f p)
       (hinv : (fderiv ℝ f p).IsInvertible) :
       ∃ e : OpenPartialHomeomorph P S,
         (e : P → S) = f ∧ p ∈ e.source ∧
         ContDiffOn ℝ ω e e.source ∧ ContDiffOn ℝ ω e.symm e.target := by
   …

3. theorem OAI.Problem356.LocalImplicit.exists_two_analytic_local_charts line 101

   Source documentation

   The two projections of a local branch can be made analytic diffeomorphisms on one common source neighborhood, contained in any prescribed neighborhood.

   theorem exists_two_analytic_local_charts
       (ψ : P → S × S) (p : P) (U : Set P) (hU : U ∈ 𝓝 p)
       (hψ : ContDiffAt ℝ ω ψ p)
       (hinv₁ : (fderiv ℝ (fun y => (ψ y).1) p).IsInvertible)
       (hinv₂ : (fderiv ℝ (fun y => (ψ y).2) p).IsInvertible) :
       ∃ e₁ e₂ : OpenPartialHomeomorph P S,
         (e₁ : P → S) = (fun y => (ψ y).1) ∧
         (e₂ : P → S) = (fun y => (ψ y).2) ∧
         p ∈ e₁.source ∧ e₁.source = e₂.source ∧ e₁.source ⊆ U ∧
         ContDiffOn ℝ ω e₁ e₁.source ∧ ContDiffOn ℝ ω e₁.symm e₁.target ∧
         ContDiffOn ℝ ω e₂ e₂.source ∧ ContDiffOn ℝ ω e₂.symm e₂.target := by
   …

4. def OAI.Problem356.LocalImplicit.implicitDerivative line 135

   Source documentation

   The derivative supplied by the implicit-function theorem, with parameter first.

   def implicitDerivative (G : P × (S × S) → S × S) (p : P) (s : S × S) :
       P →L[ℝ] S × S :=
   …

5. structure OAI.Problem356.LocalImplicit.AnalyticStationaryCharts line 141

   Source documentation

   Two separately invertible coordinates of one local stationary branch.

   structure AnalyticStationaryCharts (G : P × (S × S) → S × S) (p : P) (s : S × S) where
   …

6. theorem OAI.Problem356.LocalImplicit.nonempty_analyticStationaryCharts line 162

   Source documentation

   Local stationarity plus the three invertibility checks produces two genuine analytic charts on a common open source.

   theorem nonempty_analyticStationaryCharts
       (G : P × (S × S) → S × S) (p : P) (s : S × S)
       (hG : ContDiffAt ℝ ω G (p, s)) (hzero : G (p, s) = 0)
       (hinv : (fderiv ℝ G (p, s) ∘L ContinuousLinearMap.inr ℝ P (S × S)).IsInvertible)
       (hcentral : (ContinuousLinearMap.fst ℝ S S ∘L implicitDerivative G p s).IsInvertible)
       (hopposite : (ContinuousLinearMap.snd ℝ S S ∘L implicitDerivative G p s).IsInvertible) :
       Nonempty (AnalyticStationaryCharts G p s) := by
   …

   Mentions: OAI.Problem356.LocalImplicit.implicitDerivative, OAI.Problem356.LocalImplicit.AnalyticStationaryCharts

7. def OAI.Problem356.LocalImplicit.AnalyticStationaryCharts.restrictSource line 214

   Source documentation

   Restrict both parameter charts to the same additional open neighborhood.

   def restrictSource (c : AnalyticStationaryCharts G p s)
       (U : Set P) (hU : IsOpen U) (hp : p ∈ U) : AnalyticStationaryCharts G p s where
   …

   Mentions: OAI.Problem356.LocalImplicit.AnalyticStationaryCharts

8. theorem OAI.Problem356.LocalImplicit.AnalyticStationaryCharts.restrictSource_central_coe line 235
9. theorem OAI.Problem356.LocalImplicit.AnalyticStationaryCharts.restrictSource_opposite_coe line 239
10. theorem OAI.Problem356.LocalImplicit.AnalyticStationaryCharts.restrictSource_source line 243
11. theorem OAI.Problem356.LocalImplicit.AnalyticStationaryCharts.exists_restrict_state line 249

    Source documentation

    Any smaller open state neighborhood can be used after shrinking the common parameter domain. All chart functions and all uniqueness conclusions are preserved.

    theorem exists_restrict_state
        (c : AnalyticStationaryCharts G p s) (W : Set (S × S))
        (hW : IsOpen W) (hsW : s ∈ W) (hWV : W ⊆ c.stateDomain) :
        ∃ d : AnalyticStationaryCharts G p s,
          d.stateDomain = W ∧ d.central.source ⊆ c.central.source ∧
          (d.central : P → S) = c.central ∧ (d.opposite : P → S) = c.opposite := by
    …

    Mentions: OAI.Problem356.LocalImplicit.AnalyticStationaryCharts

12. theorem OAI.Problem356.LocalImplicit.AnalyticStationaryCharts.exists_restrict_ball line 277

    Source documentation

    The common source can be chosen to be a genuine positive-radius ball, inside any prescribed parameter neighborhood, without changing either chart function.

    theorem exists_restrict_ball
        (c : AnalyticStationaryCharts G p s) (U : Set P) (hU : U ∈ 𝓝 p) :
        ∃ r : ℝ, 0 < r ∧ ∃ d : AnalyticStationaryCharts G p s,
          d.central.source = Metric.ball p r ∧ d.central.source ⊆ U ∧
          d.stateDomain = c.stateDomain ∧
          (d.central : P → S) = c.central ∧ (d.opposite : P → S) = c.opposite := by
    …

    Mentions: OAI.Problem356.LocalImplicit.AnalyticStationaryCharts