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 dIntegrable (fun r => η ((slice i).symm (r, x))) volume d:i:Fin d.succη:𝓢(Space d.succ, )x:Space dAEStronglyMeasurable (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 dAEStronglyMeasurable (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.succIntegrable (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.succIntegrable (fun r => iteratedFDeriv n (⇑η) ((slice i).symm (r, x))) volume All goals completed! 🐙n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succIntegrable (fun a => iteratedFDeriv n (⇑η) ((slice i).symm (a, x))) volumen:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succAEStronglyMeasurable (fun r => iteratedFDeriv n (⇑η) ((slice i).symm (r, x))) volume n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succIntegrable (fun a => iteratedFDeriv n (⇑η) ((slice i).symm (a, x))) volume All goals completed! 🐙 n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succAEStronglyMeasurable (fun r => iteratedFDeriv n (⇑η) ((slice i).symm (r, x))) volume n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succContinuous fun r => iteratedFDeriv n (⇑η) ((slice i).symm (r, x)) n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succContinuous (iteratedFDeriv n η)n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succContinuous fun x_1 => (slice i).symm (x_1, x) n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succn (n + 1)n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succContDiff (n + 1) ηn:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succContinuous fun x_1 => (slice i).symm (x_1, x) exact Nat.cast_le.mpr (n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succn n + 1 All goals completed! 🐙) n:d:η:𝓢(Space d.succ, )x:Space di:Fin d.succContinuous 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 dAEStronglyMeasurable (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 dIntegrable (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 dIntegrable (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 d0 (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 d0 (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 dx ^ 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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (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 dIntegrable (fun r => fderiv (fun x => η ((slice i).symm (r, x))) x) volume All goals completed! 🐙