OAI/MathematicalPhysics/Transonic/Shooting/AxisBarriersCore.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.AxisBarriers.D line 9
2. def OAI.SepticProfile.AxisBarriers.N line 10
3. def OAI.SepticProfile.AxisBarriers.lower line 11
4. def OAI.SepticProfile.AxisBarriers.polyDen line 12
5. def OAI.SepticProfile.AxisBarriers.upper line 13
6. def OAI.SepticProfile.AxisBarriers.upperDeriv line 14
7. def OAI.SepticProfile.AxisBarriers.residualPoly line 16
8. lemma OAI.SepticProfile.AxisBarriers.radius_bounds line 22
9. lemma OAI.SepticProfile.AxisBarriers.polyDen_pos line 28
10. lemma OAI.SepticProfile.AxisBarriers.barriers_in_unit line 34
11. lemma OAI.SepticProfile.AxisBarriers.upperDeriv_pos line 54
12. lemma OAI.SepticProfile.AxisBarriers.upper_hasDeriv line 59
13. lemma OAI.SepticProfile.AxisBarriers.residualPoly_pos line 69
14. lemma OAI.SepticProfile.AxisBarriers.upper_residual_identity line 85
15. lemma OAI.SepticProfile.AxisBarriers.upper_strict_barrier line 93
16. lemma OAI.SepticProfile.AxisBarriers.lower_strict_barrier line 122
17. lemma OAI.SepticProfile.AxisBarriers.upper_lt_nine_tenths line 160
18. lemma OAI.SepticProfile.AxisBarriers.D_pos line 166
19. lemma OAI.SepticProfile.AxisBarriers.field_contDiffOn line 175
20. theorem OAI.SepticProfile.AxisBarriers.exists_between_barriers line 187

    Source documentation

    The actual regular normalized source equation can be integrated all the way to any b≤.9 while retaining the two explicit axis barriers. The clamping device is not a replacement equation: the conclusion includes its complete removal.

    theorem exists_between_barriers {sigma kappa a b u0 : ℝ}
        (hslo : (991/1000:ℝ) ≤ sigma) (hshi : sigma≤993/1000)
        (hklo : -(1/500:ℝ)≤kappa) (hkhi : kappa≤0)
        (ha : 0<a) (hab : a≤b) (hb : b≤9/10)
        (hu0 : u0 ∈ Icc (lower a) (upper a)) :
        ∃ u : ℝ → ℝ, u a=u0 ∧ ContinuousOn u (Icc a b) ∧
          (∀ t ∈ Icc a b, u t ∈ Icc (lower t) (upper t)) ∧
          ∀ t ∈ Icc a b, HasDerivWithinAt u
            (N kappa t (u t)/D sigma t (u t)) (Icc a b) t := by
    …

    Mentions: OAI.SepticProfile.sigma, OAI.SepticProfile.kappa, OAI.SepticProfile.AxisBarriers.lower, OAI.SepticProfile.AxisBarriers.upper, OAI.SepticProfile.AxisBarriers.N, OAI.SepticProfile.AxisBarriers.D