OAI/Analysis/Mahler/LevelFace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MahlerStokes.coordinateFace line 11
2. lemma OAI.MahlerStokes.contDiff_coordinateFace line 14
3. def OAI.MahlerStokes.faceLinear line 23
4. lemma OAI.MahlerStokes.hasFDerivAt_coordinateFace line 27
5. lemma OAI.MahlerStokes.faceLinear_basis line 36
6. theorem OAI.MahlerStokes.pullback_coordinateFace_coefficient line 48

   Source documentation

   The coefficient on a coordinate boundary face equals the actual pullback coefficient of its lower-dimensional parametrization.

   theorem pullback_coordinateFace_coefficient {n : ℕ} {E : Type*}
       [NormedAddCommGroup E] [NormedSpace ℝ E]
       (k : Fin (n+1)) (R : ℝ) (ψ : (Fin (n+1) → ℝ) → E)
       (ω : E → E [⋀^Fin n]→L[ℝ] ℝ) (y : Fin n → ℝ)
       (hψ : DifferentiableAt ℝ ψ (coordinateFace k R y)) :
       pullbackForm (fun z => ψ (coordinateFace k R z)) ω y (coordinateBasis n) =
         pullbackForm ψ ω (coordinateFace k R y) (k.removeNth (coordinateBasis (n+1))) := by
   …

   Mentions: OAI.MahlerStokes.coordinateFace, OAI.MahlerStokes.pullbackForm, OAI.MahlerStokes.coordinateBasis

7. def OAI.MahlerStokes.RegularBoundaryPatch.faceParam line 65
8. def OAI.MahlerStokes.RegularBoundaryPatch.faceDomain line 68
9. theorem OAI.MahlerStokes.RegularBoundaryPatch.isOpen_faceDomain line 71
10. theorem OAI.MahlerStokes.RegularBoundaryPatch.faceParam_mem line 75
11. theorem OAI.MahlerStokes.RegularBoundaryPatch.contDiffAt_faceParam line 78
12. theorem OAI.MahlerStokes.RegularBoundaryPatch.level_faceParam line 85

    Source documentation

    This parametrizes the actual regular level; the level equation is proved from the inverse chart identity.

    theorem level_faceParam (p : RegularBoundaryPatch (n+1) U g) (R : ℝ)
        {y : Fin n → ℝ} (hy : y ∈ p.faceDomain R) : g (p.faceParam R y) = R := by
    …

    Mentions: OAI.MahlerStokes.RegularBoundaryPatch

13. theorem OAI.MahlerStokes.pullback_dc_log_regular_face line 97

    Source documentation

    Real-coordinate regular charts supply actual complex-valued level parametrizations, for any chosen real continuous linear coordinate equivalence.

    theorem pullback_dc_log_regular_face {n : ℕ} {U : Set (Fin (n+1) → ℝ)}
        (Ψ : (Fin (n+1) → ℝ) ≃L[ℝ] E) (τ : E → ℝ)
        (p : RegularBoundaryPatch (n+1) U (fun x => τ (Ψ x))) {R : ℝ} (hR : 0 < R)
        {y : Fin n → ℝ} (hy : y ∈ p.faceDomain R)
        (hτ : ∀ x ∈ Ψ '' U, DifferentiableAt ℝ τ x) :
        pullbackForm (fun z => Ψ (p.faceParam R z)) (dcForm (fun x => Real.log (τ x))) y =
          R⁻¹ • pullbackForm (fun z => Ψ (p.faceParam R z)) (dcForm τ) y := by
    …

    Mentions: OAI.MahlerStokes.RegularBoundaryPatch, OAI.MahlerStokes.pullbackForm, OAI.MahlerStokes.dcForm

14. theorem OAI.MahlerStokes.pullback_ddc_log_regular_face line 108