OAI/Analysis/Mahler/CompactIntegral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompactIntegral.tube line 13
  2. lemma OAI.CompactIntegral.isOpen_tube line 15
  3. lemma OAI.CompactIntegral.local_bound line 30
  4. lemma OAI.CompactIntegral.integrable_slice line 46
  5. lemma OAI.CompactIntegral.continuousOn_integral line 53
  6. lemma OAI.CompactIntegral.hasFDerivAt_integral line 72
  7. theorem OAI.CompactIntegral.contDiffOn_integral_nat line 92

    Source documentation

    Integration over a fixed compact interval preserves every finite smoothness order. The domain consists of the parameters whose whole compact fiber is in U.

    theorem contDiffOn_integral_nat (n : ℕ) {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] {U : Set (ℂ × ℝ)} (hU : IsOpen U)
    {F : ℂ × ℝ → E} (hF : ContDiffOn ℝ n F U) :
    ContDiffOn ℝ n (fun x => ∫ t in Icc (0 : ℝ) 1, F (x,t)) (tube U) := by
…

    Mentions: OAI.CompactIntegral.tube

  8. theorem OAI.CompactIntegral.contDiffOn_integral line 115

    Source documentation

    Full joint C∞ regularity, with no domination assumption.

    theorem contDiffOn_integral {U : Set (ℂ × ℝ)} (hU : IsOpen U)
    {F : ℂ × ℝ → E} (hF : ContDiffOn ℝ ∞ F U) :
    ContDiffOn ℝ ∞ (fun x => ∫ t in Icc (0 : ℝ) 1, F (x,t)) (tube U) := by
…

    Mentions: OAI.CompactIntegral.tube