Physlib.Mathematics.Calculus.ParametricIntegration

Physlib
Mathematics
Calculus
ParametricIntegration

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
public import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
public import Mathlib.Tactic.Cases

Parametric Integration

In this module we give some lemmas around parametric integration in Lean. These extend some lemmas in Mathlib, and give them in a more physics-friendly way.

              @[expose] public section
lemma hasFDerivAt_parametric_intervalIntegral_of_contDiff
    {F : M → ℝ → N} (hf : ContDiff ℝ 1 ↿F) (x₀ : M) :
    HasFDerivAt (fun (x : M) => ∫ (t : ℝ) in 0..1, F x t ∂(volume))
      (∫ (t : ℝ) in 0..1, fderiv ℝ (F · t) x₀ ∂(volume)) x₀ := byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:M⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀
  let F' : M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (F · t) xM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) x⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀
  let s (x₀) : Set M := Metric.closedBall x₀ 1M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀
  have hF' : Continuous ↿F' := by fun_propM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀
  obtain ⟨a, ha⟩ := IsCompact.exists_isMaxOn (s := s x₀ ×ˢ Set.Icc (0 : ℝ) (1 : ℝ))
      ((isCompact_closedBall x₀ 1).prod isCompact_Icc)
      (f := fun (a : M × ℝ) => ‖F' a.1 a.2‖)
      (byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'⊢ (s x₀ ×ˢ Set.Icc 0 1).NonemptyM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀ simp [s]All goals completed! 🐙M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀)
      (continuous_norm.comp hF').continuousOnM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀
  have hx := hf.differentiable (byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) a⊢ 1 ≠ 0M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀ simpAll goals completed! 🐙M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀)M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀
  apply intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le (s := s x₀)
    (F' := F') (bound := fun t => ‖F' a.1 a.2‖)hsM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ s x₀ ∈ nhds x₀hF_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ ∀ᶠ (x : M) in nhds x₀, AEStronglyMeasurable (F x) (volume.restrict (Set.uIoc 0 1))hF_intM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ IntervalIntegrable (F x₀) volume 0 1hF'_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ AEStronglyMeasurable (F' x₀) (volume.restrict (Set.uIoc 0 1))h_boundM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ ∀ᵐ (t : ℝ), t ∈ Set.uIoc 0 1 → ∀ x ∈ s x₀, ‖F' x t‖ ≤ ‖F' a.1 a.2‖bound_integrableM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ IntervalIntegrable (fun t => ‖F' a.1 a.2‖) volume 0 1h_diffM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ ∀ᵐ (t : ℝ), t ∈ Set.uIoc 0 1 → ∀ x ∈ s x₀, HasFDerivAt (fun x => F x t) (F' x t) x
  ·hsM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ s x₀ ∈ nhds x₀ exact Metric.closedBall_mem_nhds x₀ one_posAll goals completed! 🐙
  ·hF_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ ∀ᶠ (x : M) in nhds x₀, AEStronglyMeasurable (F x) (volume.restrict (Set.uIoc 0 1)) filter_upwards with xhF_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿Fx:M⊢ AEStronglyMeasurable (F x) (volume.restrict (Set.uIoc 0 1))
    apply Continuous.aestronglyMeasurablehF_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿Fx:M⊢ Continuous (F x)
    fun_propAll goals completed! 🐙
  ·hF_intM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ IntervalIntegrable (F x₀) volume 0 1 apply Continuous.intervalIntegrablehF_intM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ Continuous (F x₀)
    fun_propAll goals completed! 🐙
  ·hF'_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ AEStronglyMeasurable (F' x₀) (volume.restrict (Set.uIoc 0 1)) apply Continuous.aestronglyMeasurablehF'_measM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ Continuous (F' x₀)
    exact Continuous.uncurry_left x₀ (byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ Continuous (Function.uncurry F') fun_propAll goals completed! 🐙)
  ·h_boundM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ ∀ᵐ (t : ℝ), t ∈ Set.uIoc 0 1 → ∀ x ∈ s x₀, ‖F' x t‖ ≤ ‖F' a.1 a.2‖ filter_upwards with t hh_boundM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1⊢ ∀ x ∈ s x₀, ‖F' x t‖ ≤ ‖F' a.1 a.2‖ xh_boundM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1x:M⊢ x ∈ s x₀ → ‖F' x t‖ ≤ ‖F' a.1 a.2‖ hxh_boundM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx✝:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1x:Mhx:x ∈ s x₀⊢ ‖F' x t‖ ≤ ‖F' a.1 a.2‖
    exact ha.2 (Set.mk_mem_prod hx (Set.Ioc_subset_Icc_self (byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx✝:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1x:Mhx:x ∈ s x₀⊢ t ∈ Set.Ioc 0 1 simpa using hAll goals completed! 🐙)))
  ·bound_integrableM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ IntervalIntegrable (fun t => ‖F' a.1 a.2‖) volume 0 1 exact intervalIntegrable_constAll goals completed! 🐙
  ·h_diffM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿F⊢ ∀ᵐ (t : ℝ), t ∈ Set.uIoc 0 1 → ∀ x ∈ s x₀, HasFDerivAt (fun x => F x t) (F' x t) x filter_upwards with t hh_diffM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1⊢ ∀ x ∈ s x₀, HasFDerivAt (fun x => F x t) (F' x t) x xh_diffM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1x:M⊢ x ∈ s x₀ → HasFDerivAt (fun x => F x t) (F' x t) x hxh_diffM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx✝:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1x:Mhx:x ∈ s x₀⊢ HasFDerivAt (fun x => F x t) (F' x t) x
    exact DifferentiableAt.hasFDerivAt (byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:MF':M → ℝ → M →L[ℝ] N := fun x t => fderiv ℝ (fun x => F x t) xs:M → Set M := fun x₀ => Metric.closedBall x₀ 1hF':Continuous ↿F'a:M × ℝha:a ∈ s x₀ ×ˢ Set.Icc 0 1 ∧ IsMaxOn (fun a => ‖F' a.1 a.2‖) (s x₀ ×ˢ Set.Icc 0 1) ahx✝:Differentiable ℝ ↿Ft:ℝh:t ∈ Set.uIoc 0 1x:Mhx:x ∈ s x₀⊢ DifferentiableAt ℝ (fun x => F x t) x fun_propAll goals completed! 🐙)

lemma fderiv_apply_parameteric_intervalIntegral
    {F : M → ℝ → N} (hf : ContDiff ℝ 1 ↿F) (x₀ : M) (v : M) :
    fderiv ℝ (fun (x : M) => ∫ (t : ℝ) in 0..1, F x t ∂(volume)) x₀ v =
      ∫ (t : ℝ) in 0..1, fderiv ℝ (F · t) x₀ v ∂(volume) := byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mv:M⊢ (fderiv ℝ (fun x => ∫ (t : ℝ) in 0..1, F x t) x₀) v = ∫ (t : ℝ) in 0..1, (fderiv ℝ (fun x => F x t) x₀) v
  rw [(hasFDerivAt_parametric_intervalIntegral_of_contDiff hf x₀).fderivM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mv:M⊢ (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) v = ∫ (t : ℝ) in 0..1, (fderiv ℝ (fun x => F x t) x₀) vM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mv:M⊢ (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) v = ∫ (t : ℝ) in 0..1, (fderiv ℝ (fun x => F x t) x₀) v]M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mv:M⊢ (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) v = ∫ (t : ℝ) in 0..1, (fderiv ℝ (fun x => F x t) x₀) v
  refine ContinuousLinearMap.intervalIntegral_apply ?_ vM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mv:M⊢ IntervalIntegrable (fun t => fderiv ℝ (fun x => F x t) x₀) volume 0 1
  apply Continuous.intervalIntegrableM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mv:M⊢ Continuous fun t => fderiv ℝ (fun x => F x t) x₀
  fun_propAll goals completed! 🐙lemma fderiv_parameteric_intervalIntegral
    {F : M → ℝ → N} (hf : ContDiff ℝ 1 ↿F) (x₀ : M) :
    fderiv ℝ (fun (x : M) => ∫ (t : ℝ) in 0..1, F x t ∂(volume)) =
      fun x => ∫ (t : ℝ) in 0..1, fderiv ℝ (F · t) x ∂(volume) := byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:M⊢ (fderiv ℝ fun x => ∫ (t : ℝ) in 0..1, F x t) = fun x => ∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x
  have h := hasFDerivAt_parametric_intervalIntegral_of_contDiff hf x₀M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mh:HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀⊢ (fderiv ℝ fun x => ∫ (t : ℝ) in 0..1, F x t) = fun x => ∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x
  ext1 xM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿Fx₀:Mh:HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x₀) x₀x:M⊢ fderiv ℝ (fun x => ∫ (t : ℝ) in 0..1, F x t) x = ∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x
  exact (hasFDerivAt_parametric_intervalIntegral_of_contDiff hf x).fderivAll goals completed! 🐙

lemma contDiff_one_parametric_intervalIntegral_of_contDiff
    {F : M → ℝ → N} (hf : ContDiff ℝ 1 ↿F) :
    ContDiff ℝ 1 (fun (x : M) => ∫ (t : ℝ) in 0..1, F x t ∂(volume)) := byM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿F⊢ ContDiff ℝ 1 fun x => ∫ (t : ℝ) in 0..1, F x t
  rw [contDiff_one_iff_hasFDerivAtM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿F⊢ ∃ f', Continuous f' ∧ ∀ (x : M), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (f' x) xM:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿F⊢ ∃ f', Continuous f' ∧ ∀ (x : M), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (f' x) x]M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿F⊢ ∃ f', Continuous f' ∧ ∀ (x : M), HasFDerivAt (fun x => ∫ (t : ℝ) in 0..1, F x t) (f' x) x
  refine ⟨_, ?_, hasFDerivAt_parametric_intervalIntegral_of_contDiff hf⟩M:TypeN:Typeinst✝⁴:NormedAddCommGroup Minst✝³:NormedSpace ℝ Minst✝²:ProperSpace Minst✝¹:NormedAddCommGroup Ninst✝:NormedSpace ℝ NF:M → ℝ → Nhf:ContDiff ℝ 1 ↿F⊢ Continuous fun x => ∫ (t : ℝ) in 0..1, fderiv ℝ (fun x => F x t) x
  fun_propAll goals completed! 🐙

lemma contDiff_succ_parametric_intervalIntegral_of_contDiff {n : ℕ} [FiniteDimensional ℝ M]
    {F : M → ℝ → N} (hf : ContDiff ℝ (n + 1) ↿F) :
    ContDiff ℝ (n + 1) (fun (x : M) => ∫ (t : ℝ) in 0..1, F x t ∂(volume)) := byM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Nn:ℕinst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ (↑n + 1) ↿F⊢ ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x t
  induction' n with n ih generalizing FzeroM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ (↑0 + 1) ↿F⊢ ContDiff ℝ (↑0 + 1) fun x => ∫ (t : ℝ) in 0..1, F x tsuccM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ ContDiff ℝ (↑(n + 1) + 1) fun x => ∫ (t : ℝ) in 0..1, F x t
  ·zeroM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ (↑0 + 1) ↿F⊢ ContDiff ℝ (↑0 + 1) fun x => ∫ (t : ℝ) in 0..1, F x t exact contDiff_one_parametric_intervalIntegral_of_contDiff hfAll goals completed! 🐙
  ·succM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ ContDiff ℝ (↑(n + 1) + 1) fun x => ∫ (t : ℝ) in 0..1, F x t rw [contDiff_succ_iff_fderivsuccM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ (Differentiable ℝ fun x => ∫ (t : ℝ) in 0..1, F x t) ∧
  (↑(n + 1) = ⊤ → AnalyticOnNhd ℝ (fun x => ∫ (t : ℝ) in 0..1, F x t) Set.univ) ∧
    ContDiff ℝ (↑(n + 1)) (fderiv ℝ fun x => ∫ (t : ℝ) in 0..1, F x t)succM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ (Differentiable ℝ fun x => ∫ (t : ℝ) in 0..1, F x t) ∧
  (↑(n + 1) = ⊤ → AnalyticOnNhd ℝ (fun x => ∫ (t : ℝ) in 0..1, F x t) Set.univ) ∧
    ContDiff ℝ (↑(n + 1)) (fderiv ℝ fun x => ∫ (t : ℝ) in 0..1, F x t)]succM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ (Differentiable ℝ fun x => ∫ (t : ℝ) in 0..1, F x t) ∧
  (↑(n + 1) = ⊤ → AnalyticOnNhd ℝ (fun x => ∫ (t : ℝ) in 0..1, F x t) Set.univ) ∧
    ContDiff ℝ (↑(n + 1)) (fderiv ℝ fun x => ∫ (t : ℝ) in 0..1, F x t)
    refine ⟨ContDiff.differentiable
      (contDiff_one_parametric_intervalIntegral_of_contDiff (hf.of_le (byM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ 1 ≤ ↑(n + 1) + 1 simpAll goals completed! 🐙))) (byM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ 1 ≠ 0 simpAll goals completed! 🐙), ?_⟩
    simp only [Nat.cast_add, Nat.cast_one, WithTop.add_eq_top, WithTop.natCast_ne_top,
      WithTop.one_ne_top, or_self, IsEmpty.forall_iff, true_and, contDiff_clm_apply_iff,
      fderiv_apply_parameteric_intervalIntegral (hf.of_le (by simp))]succM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿F⊢ ∀ (y : M), ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, (fderiv ℝ (fun x => F x t) x) y
    exact fun y => ih (byM:TypeN:Typeinst✝⁵:NormedAddCommGroup Minst✝⁴:NormedSpace ℝ Minst✝³:ProperSpace Minst✝²:NormedAddCommGroup Ninst✝¹:NormedSpace ℝ Ninst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ (↑n + 1) ↿F → ContDiff ℝ (↑n + 1) fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ (↑(n + 1) + 1) ↿Fy:M⊢ ContDiff ℝ (↑n + 1) ↿fun x t => (fderiv ℝ (fun x => F x t) x) y fun_propAll goals completed! 🐙)lemma contDiff_parametric_intervalIntegral_of_contDiff {n : ℕ} {M : Type}
    [NormedAddCommGroup M] [NormedSpace ℝ M] [ProperSpace M] [FiniteDimensional ℝ M]
    {F : M → ℝ → N} (hf : ContDiff ℝ n ↿F) :
    ContDiff ℝ n (fun (x : M) => ∫ (t : ℝ) in 0..1, F x t ∂(volume)) := byN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ Nn:ℕM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ ↑n ↿F⊢ ContDiff ℝ ↑n fun x => ∫ (t : ℝ) in 0..1, F x t
  induction' n with n ih generalizing FzeroN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ NM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ ↑0 ↿F⊢ ContDiff ℝ ↑0 fun x => ∫ (t : ℝ) in 0..1, F x tsuccN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ NM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ ↑n ↿F → ContDiff ℝ ↑n fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ ↑(n + 1) ↿F⊢ ContDiff ℝ ↑(n + 1) fun x => ∫ (t : ℝ) in 0..1, F x t
  ·zeroN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ NM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ ↑0 ↿F⊢ ContDiff ℝ ↑0 fun x => ∫ (t : ℝ) in 0..1, F x t exact contDiff_zero.mpr (byN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ NM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ MF:M → ℝ → Nhf:ContDiff ℝ ↑0 ↿F⊢ Continuous fun x => ∫ (t : ℝ) in 0..1, F x t fun_propAll goals completed! 🐙)
  ·succN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ NM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ ↑n ↿F → ContDiff ℝ ↑n fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ ↑(n + 1) ↿F⊢ ContDiff ℝ ↑(n + 1) fun x => ∫ (t : ℝ) in 0..1, F x t exact contDiff_succ_parametric_intervalIntegral_of_contDiff (hf.of_le (byN:Typeinst✝⁵:NormedAddCommGroup Ninst✝⁴:NormedSpace ℝ NM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:ProperSpace Minst✝:FiniteDimensional ℝ Mn:ℕih:∀ {F : M → ℝ → N}, ContDiff ℝ ↑n ↿F → ContDiff ℝ ↑n fun x => ∫ (t : ℝ) in 0..1, F x tF:M → ℝ → Nhf:ContDiff ℝ ↑(n + 1) ↿F⊢ ↑n + 1 ≤ ↑(n + 1) simpAll goals completed! 🐙))