OAI/Analysis/BernoulliCone/JointIntervalIntegral.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Bernoulli.ParametricIntegral.fixed_hasFDerivAt line 18

   Source documentation

   A compact-interval parameter derivative, with domination obtained from C1 on an actual compact product. No derivative bound is an extra premise.

   theorem fixed_hasFDerivAt {F:E×ℝ→G} (hF:ContDiff ℝ 1 F) (x:E) (a b:ℝ) :
       HasFDerivAt (fun y:E=>∫t in a..b,F (y,t))
         (∫t in a..b,fderiv ℝ F (x,t) ∘L ContinuousLinearMap.inl ℝ E ℝ) x := by
   …

2. def OAI.Bernoulli.ParametricIntegral.heightPrimitive line 42
3. lemma OAI.Bernoulli.ParametricIntegral.heightPrimitive_rescale line 45
4. theorem OAI.Bernoulli.ParametricIntegral.heightPrimitive_differentiable line 57

   Source documentation

   Joint differentiability is proved, rather than inferred from separate partial derivatives. Rescaling to [0,1] gives a compact dominated derivative.

   theorem heightPrimitive_differentiable [CompleteSpace G] {F:E×ℝ→G} (hF:ContDiff ℝ 1 F) :
       Differentiable ℝ (heightPrimitive F) := by
   …

   Mentions: OAI.Bernoulli.ParametricIntegral.heightPrimitive

5. lemma OAI.Bernoulli.ParametricIntegral.heightPrimitive_height line 69
6. lemma OAI.Bernoulli.ParametricIntegral.heightPrimitive_fderiv line 74
7. lemma OAI.Bernoulli.ParametricIntegral.graph_fderiv line 97