Imports
/- Copyright (c) 2025 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 Physlib.SpaceAndTime.Space.Derivatives.Basic public import Physlib.SpaceAndTime.Space.Slice public import Mathlib.Analysis.Calculus.ParametricIntegral

Constant slice distributions

i. Overview

In this module we define the lift of distributions on Space d to distributions on Space d.succ which are constant between slices in the ith direction.

This is used, for example, to define distributions which are translationally invariant in the ith direction.

Examples of distributions which can be constructed in this way include the dirac deltas for lines and planes, rather then points.

ii. Key results

    sliceSchwartz : The continuous linear map which takes a Schwartz map on Space d.succ and gives a Schwartz map on Space d by integrating over the ith direction.

    constantSliceDist : The distribution on Space d.succ formed by a distribution on Space d which is translationally invariant in the ith direction.

iii. Table of contents

    A. Schwartz maps

      A.1. Bounded condition for derivatives of Schwartz maps on slices

      A.2. Integrability for of Schwartz maps on slices

      A.3. Continiuity of integrations of slices of Schwartz maps

      A.4. Derivative of integrations of slices of Schwartz maps

      A.5. Differentiability as a slices of Schwartz maps

      A.6. Smoothness as slices of Schwartz maps

      A.7. Iterated derivatives of integrations of slices of Schwartz maps

      A.8. The map integrating over one component of a Schwartz map

    B. Constant slice distribution

      B.1. Derivative of constant slice distributions

iv. References

@[expose] public section

A. Schwartz maps

A.1. Bounded condition for derivatives of Schwartz maps on slices

All goals completed! 🐙 n:ℕm:ℕd:ℕi:Fin d.succrt:ℕhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumeη:𝓢(Space d.succ, ℝ)h0:∀ (x : Space (d + 1)), (1 + ‖x‖) ^ (rt + m) * ‖iteratedFDeriv ℝ n (⇑η) x‖ ≤ 2 ^ (rt + m) * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝ := 2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηx:Space dr:ℝ⊢ (1 + ‖(slice i).symm (r, x)‖) ^ m * (1 + ‖(slice i).symm (r, x)‖) ^ rt = (1 + ‖(slice i).symm (r, x)‖) ^ (rt + m) All goals completed! 🐙

A.2. Integrability for of Schwartz maps on slices

d:ℕn:ℕm:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηt:ℝ⊢ ‖(slice i).symm (t, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (t, x))‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹ All goals completed! 🐙lemma schwartzMap_integrable_slice_symm {d : ℕ} (i : Fin d.succ) (η : 𝓢(Space d.succ, ℝ)) (x : Space d) : Integrable (fun r => η ((slice i).symm (r, x))) volume := d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun r => η ((slice i).symm (r, x))) volume d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)x:Space d⊢ AEStronglyMeasurable (fun r => η ((slice i).symm (r, x))) volumed:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)x:Space d⊢ ∀ᵐ (a : ℝ), ‖‖(slice i).symm (a, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (a, x))‖‖ = ‖η ((slice i).symm (a, x))‖ d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)x:Space d⊢ AEStronglyMeasurable (fun r => η ((slice i).symm (r, x))) volume All goals completed! 🐙 d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)x:Space d⊢ ∀ᵐ (a : ℝ), ‖‖(slice i).symm (a, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (a, x))‖‖ = ‖η ((slice i).symm (a, x))‖ All goals completed! 🐙d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝheq:fderiv ℝ (fun x => (slice i).symm (r, x)) x = ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))⊢ ‖fderiv ℝ (⇑η) ((slice i).symm (r, x)) ∘SL ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ≤ ‖fderiv ℝ (⇑η) ((slice i).symm (r, x))‖ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝheq:fderiv ℝ (fun x => (slice i).symm (r, x)) x = ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))⊢ DifferentiableAt ℝ (⇑η) ((slice i).symm (r, x)) d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝheq:fderiv ℝ (fun x => (slice i).symm (r, x)) x = ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))⊢ ‖fderiv ℝ (⇑η) ((slice i).symm (r, x)) ∘SL ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ≤ ‖fderiv ℝ (⇑η) ((slice i).symm (r, x))‖ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ All goals completed! 🐙 d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝheq:fderiv ℝ (fun x => (slice i).symm (r, x)) x = ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))⊢ DifferentiableAt ℝ (⇑η) ((slice i).symm (r, x)) All goals completed! 🐙@[fun_prop] lemma schwartzMap_fderiv_left_integrable_slice_symm {d : ℕ} (η : 𝓢(Space d.succ, ℝ)) (x : Space d) (i : Fin d.succ) : Integrable (fun r => fderiv ℝ (fun r => η (((slice i).symm (r, x)))) r 1) volume := d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Integrable (fun r => (fderiv ℝ (fun r => η ((slice i).symm (r, x))) r) 1) volume conv_lhs => d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ| (fderiv ℝ (fun r => η ((slice i).symm (r, x))) r) 1 d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ| (fderiv ℝ (fun r => η ((slice i).symm (r, x))) r) 1 d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ| (fderiv ℝ (⇑η ∘ fun r => (slice i).symm (r, x)) r) 1 rw [fderiv_comp _ η.differentiableAt (d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ⊢ DifferentiableAt ℝ (fun r => (slice i).symm (r, x)) r All goals completed! 🐙)] d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ| (fderiv ℝ (⇑η) ((slice i).symm (r, x))) ((slice i).symm (1, 0)) d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ| ((SchwartzMap.evalCLM ℝ (Space d.succ) ℝ ((slice i).symm (1, 0)) ∘SL fderivCLM ℝ (Space d.succ) ℝ) η) ((slice i).symm (r, x)) d:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succr:ℝ| ((LineDeriv.lineDerivOpCLM ℝ 𝓢(Space d.succ, ℝ) ((slice i).symm (1, 0))) η) ((slice i).symm (r, x)) All goals completed! 🐙@[fun_prop] lemma schwartzMap_iteratedFDeriv_norm_slice_symm_integrable {n} {d : ℕ} (η : 𝓢(Space d.succ, ℝ)) (x : Space d) (i : Fin d.succ) : Integrable (fun r => ‖iteratedFDeriv ℝ n ⇑η (((slice i).symm (r, x)))‖) volume := n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Integrable (fun r => ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) volume All goals completed! 🐙n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Integrable (fun a => ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (a, x))‖) volumen:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ AEStronglyMeasurable (fun r => iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) volume n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Integrable (fun a => ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (a, x))‖) volume All goals completed! 🐙 n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ AEStronglyMeasurable (fun r => iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) volume n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Continuous fun r => iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x)) n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Continuous (iteratedFDeriv ℝ n ⇑η)n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Continuous fun x_1 => (slice i).symm (x_1, x) n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ ↑n ≤ ↑(n + 1)n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ ContDiff ℝ ↑(n + 1) ⇑ηn:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Continuous fun x_1 => (slice i).symm (x_1, x) exact Nat.cast_le.mpr (n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ n ≤ n + 1 All goals completed! 🐙) n:ℕd:ℕη:𝓢(Space d.succ, ℝ)x:Space di:Fin d.succ⊢ Continuous fun x_1 => (slice i).symm (x_1, x) All goals completed! 🐙

A.3. Continiuity of integrations of slices of Schwartz maps

lemma continuous_schwartzMap_slice_integral {d} (i : Fin d.succ) (η : 𝓢(Space d.succ, ℝ)) : Continuous (fun x : Space d => ∫ r : ℝ, η ((slice i).symm (r, x))) := d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)⊢ Continuous fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Continuous fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Continuous fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ (x : Space d), AEStronglyMeasurable (fun a => η ((slice i).symm (a, x))) volumed:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ (x : Space d), ∀ᵐ (a : ℝ), ‖η ((slice i).symm (a, x))‖ ≤ k * ‖(1 + ‖a‖) ^ rt‖⁻¹d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Integrable (fun t => k * ‖(1 + ‖t‖) ^ rt‖⁻¹) volumed:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ᵐ (a : ℝ), Continuous fun x => η ((slice i).symm (a, x)) d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ (x : Space d), AEStronglyMeasurable (fun a => η ((slice i).symm (a, x))) volume d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηx:Space d⊢ AEStronglyMeasurable (fun a => η ((slice i).symm (a, x))) volume All goals completed! 🐙 d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ (x : Space d), ∀ᵐ (a : ℝ), ‖η ((slice i).symm (a, x))‖ ≤ k * ‖(1 + ‖a‖) ^ rt‖⁻¹ d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηx:Space d⊢ ∀ᵐ (a : ℝ), ‖η ((slice i).symm (a, x))‖ ≤ k * ‖(1 + ‖a‖) ^ rt‖⁻¹ d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηx:Space dt:ℝ⊢ ‖η ((slice i).symm (t, x))‖ ≤ k * ‖(1 + ‖t‖) ^ rt‖⁻¹ All goals completed! 🐙 d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Integrable (fun t => k * ‖(1 + ‖t‖) ^ rt‖⁻¹) volume d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Integrable (fun x => ‖(1 + ‖x‖) ^ rt‖⁻¹) volume All goals completed! 🐙 d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ᵐ (a : ℝ), Continuous fun x => η ((slice i).symm (a, x)) d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)rt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 0).1 * ((Finset.Iic (rt + 0, 0)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηt:ℝ⊢ Continuous fun x => η ((slice i).symm (t, x)) All goals completed! 🐙

A.4. Derivative of integrations of slices of Schwartz maps

d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηr:ℝx:Space da✝:x ∈ fun a => HasFDerivAtFilter (fun x => F x (F x₀ 0)) (F' a (F x₀ 0)) (nhds a ×ˢ pure a)hb:‖fderiv ℝ (fun x => η ((slice i).symm (r, x))) x‖ ≤ ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖⊢ ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηr:ℝx:Space da✝:x ∈ fun a => HasFDerivAtFilter (fun x => F x (F x₀ 0)) (F' a (F x₀ 0)) (nhds a ×ˢ pure a)hb:‖fderiv ℝ (fun x => η ((slice i).symm (r, x))) x‖ ≤ ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖⊢ ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹ All goals completed! 🐙 d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Integrable (fun t => k * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ * ‖(1 + ‖t‖) ^ rt‖⁻¹) volume d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ Integrable (fun x => ‖(1 + ‖x‖) ^ rt‖⁻¹) volume All goals completed! 🐙 d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η⊢ ∀ᵐ (a : ℝ), ∀ x ∈ fun a => HasFDerivAtFilter (fun x => F x (F x₀ 0)) (F' a (F x₀ 0)) (nhds a ×ˢ pure a), HasFDerivAt (fun x => F x a) (F' x a) x d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηt:ℝ⊢ ∀ x ∈ fun a => HasFDerivAtFilter (fun x => F x (F x₀ 0)) (F' a (F x₀ 0)) (nhds a ×ˢ pure a), HasFDerivAt (fun x => F x t) (F' x t) x d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx₀:Space dF:Space d → ℝ → ℝ := fun x r => η ((slice i).symm (r, x))F':Space d → ℝ → Space d →L[ℝ] ℝ := fun x₀ r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x₀hF:∀ (t : ℝ) (x : Space d), HasFDerivAt (fun x => F x t) (F' x t) xrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ 0 * ‖iteratedFDeriv ℝ 1 (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹k_eq:k = 2 ^ (rt + 0, 1).1 * ((Finset.Iic (rt + 0, 1)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηt:ℝx:Space da✝:x ∈ fun a => HasFDerivAtFilter (fun x => F x (F x₀ 0)) (F' a (F x₀ 0)) (nhds a ×ˢ pure a)⊢ HasFDerivAt (fun x => F x t) (F' x t) x All goals completed! 🐙

A.5. Differentiability as a slices of Schwartz maps

lemma schwartzMap_slice_integral_differentiable {d : ℕ} (η : 𝓢(Space d.succ, ℝ)) (i : Fin d.succ) : Differentiable ℝ (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) := fun x => (schwartzMap_slice_integral_hasFDerivAt η i x).differentiableAt

A.6. Smoothness as slices of Schwartz maps

d:ℕi:Fin d.succn:ℕih:∀ (η : 𝓢(Space d.succ, ℝ)), ContDiff ℝ ↑n fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))η:𝓢(Space d.succ, ℝ)y:Space dhl:(fun x => (∫ (r : ℝ), fderiv ℝ (fun x => η ((slice i).symm (r, x))) x) y) = fun x => ∫ (r : ℝ), (fderiv ℝ (fun x => η ((slice i).symm (r, x))) x) yhl2:(fun x => ∫ (r : ℝ), (fderiv ℝ (fun x => η ((slice i).symm (r, x))) x) y) = fun x => ∫ (r : ℝ), ((LineDeriv.lineDerivOpCLM ℝ 𝓢(Space d.succ, ℝ) ((slice i).symm (0, y))) η) ((slice i).symm (r, x))⊢ ContDiff ℝ ↑n fun x => ∫ (r : ℝ), ((LineDeriv.lineDerivOpCLM ℝ 𝓢(Space d.succ, ℝ) ((slice i).symm (0, y))) η) ((slice i).symm (r, x)) All goals completed! 🐙 d:ℕi:Fin d.succn:ℕih:∀ (η : 𝓢(Space d.succ, ℝ)), ContDiff ℝ ↑n fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))η:𝓢(Space d.succ, ℝ)⊢ ∀ (x : Space d), HasFDerivAt (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) (∫ (r : ℝ), fderiv ℝ (fun x => η ((slice i).symm (r, x))) x) x All goals completed! 🐙

A.7. Iterated derivatives of integrations of slices of Schwartz maps

d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ (fderiv ℝ (fun x => (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, Fin.tail y j)) x) (y 0) = (fderiv ℝ (fun x => (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) (Fin.tail fun j => (slice i).symm (0, y j))) x) (y 0)d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ DifferentiableAt ℝ (fun y_1 => (iteratedFDeriv ℝ n (⇑η) y_1) (Fin.tail fun j => (slice i).symm (0, y j))) ((slice i).symm (r, x))d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ n ⇑η) ((slice i).symm (r, x)) d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ DifferentiableAt ℝ (fun y_1 => (iteratedFDeriv ℝ n (⇑η) y_1) (Fin.tail fun j => (slice i).symm (0, y j))) ((slice i).symm (r, x))d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ n ⇑η) ((slice i).symm (r, x)) d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ DifferentiableAt ℝ (fun y_1 => (iteratedFDeriv ℝ n (⇑η) y_1) (Fin.tail fun j => (slice i).symm (0, y j))) ((slice i).symm (r, x)) All goals completed! 🐙 d:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succn:ℕih:∀ (x : Space d) (y : Fin n → Space d), (iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x) y = ∫ (r : ℝ), (iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) fun j => (slice i).symm (0, y j)x:Space dy:Fin (n + 1) → Space dhdiff:Differentiable ℝ (iteratedFDeriv ℝ n ⇑η)r:ℝ⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ n ⇑η) ((slice i).symm (r, x)) All goals completed! 🐙d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space dy:Fin n → Space d⊢ ((∫ (x_1 : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (x_1, x))) fun j => (slice i).symm (0, y j)) = ((∫ (r : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))).compContinuousLinearMap fun x => ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))) yd:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space dy:Fin n → Space d⊢ Integrable (fun r => iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) volume d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space dy:Fin n → Space d⊢ ((∫ (x_1 : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (x_1, x))) fun j => (slice i).symm (0, y j)) = ((∫ (r : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))).compContinuousLinearMap fun x => ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))) y All goals completed! 🐙 d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space dy:Fin n → Space d⊢ Integrable (fun r => iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))) volume All goals completed! 🐙d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space d⊢ ‖(∫ (r : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))).compContinuousLinearMap fun x => ↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ≤ (∫ (r : ℝ), ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space d⊢ ‖∫ (r : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ * ∏ i_1, ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ≤ (∫ (r : ℝ), ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space d⊢ ‖∫ (r : ℝ), iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n ≤ (∫ (r : ℝ), ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n refine mul_le_mul ?_ (d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space d⊢ ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n ≤ ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n All goals completed! 🐙) (d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space d⊢ 0 ≤ ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n All goals completed! 🐙) (d:ℕn:ℕη:𝓢(Space d.succ, ℝ)i:Fin d.succx:Space d⊢ 0 ≤ ∫ (r : ℝ), ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ All goals completed! 🐙) All goals completed! 🐙d:ℕn:ℕm:ℕi:Fin d.succrt:ℕhrt✝:∀ (η : 𝓢(Space d.succ, ℝ)), ∃ k, Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ (∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹) ∧ k = 2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) ηη:𝓢(Space d.succ, ℝ)x:Space dk:ℝhrt:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:∀ (x : Space d) (r : ℝ), ‖(slice i).symm (r, x)‖ ^ m * ‖iteratedFDeriv ℝ n (⇑η) ((slice i).symm (r, x))‖ ≤ k * ‖(1 + ‖r‖) ^ rt‖⁻¹hk:2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η = k⊢ (k * ∫ (a : ℝ), ‖((1 + ‖a‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n = (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * k All goals completed! 🐙

A.8. The map integrating over one component of a Schwartz map

The continuous linear map taking a Schwartz map and integrating over the ith component, to give a Schwartz map of one dimension lower.

All goals completed! 🐙 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ ∀ (f : 𝓢(Space d.succ, ℝ)), ContDiff ℝ ↑⊤ fun x => ∫ (r : ℝ), f ((slice i).symm (r, x)) 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)⊢ ContDiff ℝ ↑⊤ fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)⊢ ContDiff ℝ ↑⊤ fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)⊢ ∀ (n : ℕ), ContDiff ℝ ↑n fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)n:ℕ⊢ ContDiff ℝ ↑n fun x => ∫ (r : ℝ), η ((slice i).symm (r, x)) All goals completed! 🐙 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ ∀ (n : ℕ × ℕ), ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(Space d.succ, ℝ)) (x : Space d), ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ (Space d.succ) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succ⊢ ∀ (a b : ℕ), ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(Space (d + 1), ℝ)) (x : Space d), ‖x‖ ^ a * ‖iteratedFDeriv ℝ b (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕ⊢ ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(Space (d + 1), ℝ)) (x : Space d), ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ ∃ s C, 0 ≤ C ∧ ∀ (f : 𝓢(Space (d + 1), ℝ)) (x : Space d), ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ ∃ C, 0 ≤ C ∧ ∀ (f : 𝓢(Space (d + 1), ℝ)) (x : Space d), ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ C * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ 0 ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n ∧ ∀ (f : 𝓢(Space (d + 1), ℝ)) (x : Space d), ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ 0 ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ ∀ (f : 𝓢(Space (d + 1), ℝ)) (x : Space d), ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), f ((slice i).symm (r, x))) x‖ ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) f 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ 0 ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n All goals completed! 🐙 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)η:𝓢(Space (d + 1), ℝ)x:Space d⊢ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) η 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)η:𝓢(Space (d + 1), ℝ)x:Space dhrt1:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) η 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)η:𝓢(Space (d + 1), ℝ)x:Space dhrt1:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η) ≤ (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) η 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)η:𝓢(Space (d + 1), ℝ)x:Space dhrt1:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η) = (2 ^ (rt + m, n).1 * ∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) η 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕi:Fin d.succm:ℕn:ℕrt:ℕhrt:∀ (η : 𝓢(Space d.succ, ℝ)) (x : Space d), Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volume ∧ ‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)η:𝓢(Space (d + 1), ℝ)x:Space dhrt1:Integrable (fun x => ‖((1 + ‖x‖) ^ rt)⁻¹‖) volumehbound:‖x‖ ^ m * ‖iteratedFDeriv ℝ n (fun x => ∫ (r : ℝ), η ((slice i).symm (r, x))) x‖ ≤ (∫ (r : ℝ), ‖((1 + ‖r‖) ^ rt)⁻¹‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * (2 ^ (rt + m, n).1 * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η)⊢ (∫ (r : ℝ), ‖(1 + ‖r‖)⁻¹ ^ rt‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup fun m => SchwartzMap.seminorm ℝ m.1 m.2) η * 2 ^ rt * 2 ^ m = (∫ (r : ℝ), ‖(1 + ‖r‖)⁻¹ ^ rt‖) * ‖↑(slice i).symm ∘SL ContinuousLinearMap.prod 0 (ContinuousLinearMap.id ℝ (Space d))‖ ^ n * ((Finset.Iic (rt + m, n)).sup (schwartzSeminormFamily ℝ (Space (d + 1)) ℝ)) η * 2 ^ rt * 2 ^ m All goals completed! 🐙
lemma sliceSchwartz_apply {d : ℕ} (i : Fin d.succ) (η : 𝓢(Space d.succ, ℝ)) (x : Space d) : sliceSchwartz i η x = ∫ (r : ℝ), η ((slice i).symm (r, x)) := d:ℕi:Fin d.succη:𝓢(Space d.succ, ℝ)x:Space d⊢ ((sliceSchwartz i) η) x = ∫ (r : ℝ), η ((slice i).symm (r, x)) All goals completed! 🐙

B. Constant slice distribution

Distributions on Space d.succ from distributions on Space d given a direction i. These distributions are constant on slices in the i direction..

def constantSliceDist {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) : ((Space d) →d[ℝ] M) →ₗ[ℝ] (Space d.succ) →d[ℝ] M where toFun f := f ∘L sliceSchwartz i map_add' f g := 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁷:RCLike 𝕜inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedAddCommGroup F'inst✝³:NormedSpace ℝ Einst✝²:NormedSpace ℝ FM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mg:(Space d)→d[ℝ] M⊢ (f + g) ∘SL sliceSchwartz i = f ∘SL sliceSchwartz i + g ∘SL sliceSchwartz i 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁷:RCLike 𝕜inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedAddCommGroup F'inst✝³:NormedSpace ℝ Einst✝²:NormedSpace ℝ FM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mg:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)⊢ ((f + g) ∘SL sliceSchwartz i) η = (f ∘SL sliceSchwartz i + g ∘SL sliceSchwartz i) η All goals completed! 🐙 map_smul' c f := 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁷:RCLike 𝕜inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedAddCommGroup F'inst✝³:NormedSpace ℝ Einst✝²:NormedSpace ℝ FM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succc:ℝf:(Space d)→d[ℝ] M⊢ (c • f) ∘SL sliceSchwartz i = (RingHom.id ℝ) c • f ∘SL sliceSchwartz i 𝕜:TypeE:TypeF:TypeF':Typeinst✝⁷:RCLike 𝕜inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedAddCommGroup F'inst✝³:NormedSpace ℝ Einst✝²:NormedSpace ℝ FM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succc:ℝf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)⊢ ((c • f) ∘SL sliceSchwartz i) η = ((RingHom.id ℝ) c • f ∘SL sliceSchwartz i) η All goals completed! 🐙
lemma constantSliceDist_apply {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (i : Fin d.succ) (f : (Space d) →d[ℝ] M) (η : 𝓢(Space d.succ, ℝ)) : constantSliceDist i f η = f (sliceSchwartz i η) := M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)⊢ ((constantSliceDist i) f) η = f ((sliceSchwartz i) η) All goals completed! 🐙

B.1. Derivative of constant slice distributions

M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => (fderiv ℝ (fun r => 1) x_1) 1 * η ((slice i).symm (x_1, x))) volumeM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => 1 * (fderiv ℝ (fun r => η ((slice i).symm (r, x))) x_1) 1) volumeM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => 1 * η ((slice i).symm (x_1, x))) volumeM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ ∀ x_1 ∈ tsupport fun r => η ((slice i).symm (r, x)), DifferentiableAt ℝ (fun r => 1) x_1M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ ∀ x_1 ∈ tsupport fun r => 1, DifferentiableAt ℝ (fun r => η ((slice i).symm (r, x))) x_1 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => (fderiv ℝ (fun r => 1) x_1) 1 * η ((slice i).symm (x_1, x))) volume All goals completed! 🐙 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => 1 * (fderiv ℝ (fun r => η ((slice i).symm (r, x))) x_1) 1) volume M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => _root_.deriv (fun r => η ((slice i).symm (r, x))) x_1) volume M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun r => (fderiv ℝ (fun r => η ((slice i).symm (r, x))) r) 1) volume All goals completed! 🐙 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => 1 * η ((slice i).symm (x_1, x))) volume M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ Integrable (fun x_1 => η ((slice i).symm (x_1, x))) volume All goals completed! 🐙 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ ∀ x_1 ∈ tsupport fun r => η ((slice i).symm (r, x)), DifferentiableAt ℝ (fun r => 1) x_1 All goals completed! 🐙 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succf:(Space d)→d[ℝ] Mη:𝓢(Space d.succ, ℝ)x:Space d⊢ ∀ x_1 ∈ tsupport fun r => 1, DifferentiableAt ℝ (fun r => η ((slice i).symm (r, x))) x_1 All goals completed! 🐙 All goals completed! 🐙M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succj:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space (d + 1), ℝ)x:Space dr:ℝ⊢ DifferentiableAt ℝ (⇑η) ((slice i).symm (r, x))M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succj:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space (d + 1), ℝ)x:Space d⊢ Integrable (fun r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x) volume M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succj:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space (d + 1), ℝ)x:Space dr:ℝ⊢ DifferentiableAt ℝ (⇑η) ((slice i).symm (r, x)) All goals completed! 🐙 M:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Md:ℕi:Fin d.succj:Fin df:(Space d)→d[ℝ] Mη:𝓢(Space (d + 1), ℝ)x:Space d⊢ Integrable (fun r => fderiv ℝ (fun x => η ((slice i).symm (r, x))) x) volume All goals completed! 🐙