OAI/Analysis/BernoulliCone/CapCalculus.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V_bounds line 11
  2. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_V line 22
  3. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_D line 27
  4. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_E line 30
  5. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_H line 33
  6. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V_contDiff line 38
  7. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.H_contDiff line 40
  8. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Y line 44

    Source documentation

    The cap prefactor in squared transverse coordinates.

    def Y (q b C:ℝ) :ℝ := C*V q b/Real.sqrt (H q b)

    Mentions: OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V, OAI.Bernoulli.DeSilvaJerison.CapAlgebra.H

  9. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Y1 line 45
  10. def OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Y2 line 47
  11. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Y_contDiffAt line 51
  12. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_Y line 54
  13. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_Y1 line 60
  14. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.deriv_Y line 71
  15. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.deriv2_Y line 72
  16. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.hasDerivAt_invV line 78
  17. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.deriv2_invV line 82
  18. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.lap_Y line 94
  19. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.invV_mixed line 113
  20. lemma OAI.Bernoulli.DeSilvaJerison.capH_contDiff line 133
  21. lemma OAI.Bernoulli.DeSilvaJerison.deriv2_capH line 145
  22. def OAI.Bernoulli.DeSilvaJerison.capC line 150
  23. def OAI.Bernoulli.DeSilvaJerison.smoothCap line 151
  24. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_contDiffAt line 154
  25. lemma OAI.Bernoulli.DeSilvaJerison.laplacian_smoothCap line 161
  26. lemma OAI.Bernoulli.DeSilvaJerison.cap_sHP_nonpos line 221
  27. theorem OAI.Bernoulli.DeSilvaJerison.smoothCap_laplacian_nonpos line 228

    Source documentation

    The actual smooth cylindrical cap is superharmonic on its positive strip.

    theorem smoothCap_laplacian_nonpos {x:Space 7} (hx:Cylindrical.radiusSq axis x≤1)
    (hs:|Cylindrical.axis axis x/CapAlgebra.V (Cylindrical.radiusSq axis x) capB|≤3/4) :
    Δ smoothCap x≤0 := by
…

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.Cylindrical.axis, OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V, OAI.Bernoulli.DeSilvaJerison.capB, OAI.Bernoulli.DeSilvaJerison.smoothCap