Mathlib.Analysis.Calculus.FiniteProduct
This package gives explicit coordinate-specific Leibniz formulas, derivative certificates, support-visible decompositions, and elementary bounds for mixed jets of finite products of real-valued two-coordinate functions.
Basic 11 core · 0 supporting Two lists record which factors each coordinate differentiation hits.
Coordinate finite-product jets: explicit ordered-hit formulas
Two lists record which factors each coordinate differentiation hits. Repeated hits are counted, rather than collapsed to a set. The seven supplied factor jets suffice: second second-coordinate derivatives at first-coordinate orders zero and one are zero. Ordered pairs of first-coordinate hits automatically give coefficient two for distinct factors, without division or nonvanishing assumptions. All sums are explicit finite sums.
structure FactorJets reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
A family of factor jets on an index type supplies the base, first-coordinate, and second-coordinate functions needed through order two in each coordinate.
Definition (Lean source)
parameters
ι :
Type*
fields
f00 :
ι → ℝ → ℝ → ℝ
f10 :
ι → ℝ → ℝ → ℝ
f20 :
ι → ℝ → ℝ → ℝ
f01 :
ι → ℝ → ℝ → ℝ
f11 :
ι → ℝ → ℝ → ℝ
f21 :
ι → ℝ → ℝ → ℝ
f22 :
ι → ℝ → ℝ → ℝ
def factorJet reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The selected factor jet of a supplied family at an index, two derivative orders, and a point is the supplied function for that pair of orders when the pair is one of (0,0), (1,0), (2,0), (0,1), (1,1), (2,1), (2,2), and zero for every other pair.
Definition (Lean source)
parameters
def
factorJet J i p q a u :
ℝ
given by
match p, q with | 0, 0
=> J.f00 i a u | 1, 0 => J.f10 i a u | 2, 0 => J.f20 i a u | 0, 1 => J.f01 i a u | 1, 1 => J.f11 i a u | 2, 1 => J.f21 i a u | 2, 2 => J.f22 i a u | _, _ => 0
def leibnizTerm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
An ordered-hit Leibniz summand for a finite set, factor jets, first and second coordinate hit lists, and a point is the product, over the indices in the finite set, of each factor's jet at the point whose first- and second-coordinate orders are the numbers of times that index occurs in the first and second hit lists. Thus the derivative assignments are inspectable factor by factor.
Definition (Lean source)
parameters
def
leibnizTerm I J xs ys a u :
ℝ
given by
∏ i ∈ I, factorJet J i (xs.count i) (ys.count i) a u
def product reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The finite product of the factors over a finite index set is evaluated at a point.
Definition (Lean source)
parameters
def
product I J a u :
ℝ
given by
∏ i ∈ I, J.f00 i a u
def productJet10 reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The first first-coordinate jet of the finite product at a point sums over the factor hit by one differentiation.
Definition (Lean source)
def productJet20 reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The second first-coordinate jet of the finite product at a point sums over two ordered first-coordinate hits. Equal hits use the second jet of one factor; distinct hits use the first jets of two factors.
Definition (Lean source)
def productJet21 reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The mixed jet of orders two and one of the finite product at a point sums over two ordered first-coordinate hits and one second-coordinate hit.
Definition (Lean source)
parameters
def
productJet21 I J a u :
ℝ
given by
∑ i ∈ I, ∑ j ∈ I, ∑ k ∈ I, leibnizTerm I J [i, j] [k] a u
def productJet22 reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The mixed jet of orders two and two of the finite product at a point sums over four ordered hits. Repeated second-coordinate hits vanish unless all four hits are the same factor, which supplies its (2,2) jet.
Definition (Lean source)
parameters
def
productJet22 I J a u :
ℝ
given by
∑ i ∈ I, ∑ j ∈ I, ∑ k ∈ I, ∑ l ∈ I, leibnizTerm I J [i, j] [k, l] a u
structure AChainsAt reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
First-coordinate derivative data for a finite family at a point consists of the derivative from the base factor to its first jet and the derivative from that first jet to its second jet.
Definition (Lean source)
parameters
assumes
da00 :
∀ i ∈ I, HasDerivAt (fun b => J.f00 i b u) (J.f10 i a u) a
da10 :
∀ i ∈ I, HasDerivAt (fun b => J.f10 i b u) (J.f20 i a u) a
structure UChainsAt reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
Second-coordinate derivative data for a finite family at a point consists of the six required factor derivative identities. The zero derivatives of the (0,1) and (1,1) jets express second-coordinate affinity.
Definition (Lean source)
parameters
assumes
du00 :
∀ i ∈ I, HasDerivAt (J.f00 i a) (J.f01 i a u) u
du01 :
∀ i ∈ I, HasDerivAt (J.f01 i a) 0 u
du10 :
∀ i ∈ I, HasDerivAt (J.f10 i a) (J.f11 i a u) u
du11 :
∀ i ∈ I, HasDerivAt (J.f11 i a) 0 u
du20 :
∀ i ∈ I, HasDerivAt (J.f20 i a) (J.f21 i a u) u
du21 :
∀ i ∈ I, HasDerivAt (J.f21 i a) (J.f22 i a u) u
structure FactorBoundsAt reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
Factor envelopes for a finite family at a point consist of the bound of two on the base factors and the bounds of four on the six positive-order jets.
Definition (Lean source)
parameters
assumes
bound00 :
∀ i ∈ I, |J.f00 i a u| ≤ 2
bound10 :
∀ i ∈ I, |J.f10 i a u| ≤ 4
bound20 :
∀ i ∈ I, |J.f20 i a u| ≤ 4
bound01 :
∀ i ∈ I, |J.f01 i a u| ≤ 4
bound11 :
∀ i ∈ I, |J.f11 i a u| ≤ 4
bound21 :
∀ i ∈ I, |J.f21 i a u| ≤ 4
bound22 :
∀ i ∈ I, |J.f22 i a u| ≤ 4
Bounds 1 core · 3 supporting An ordered-hit term has at most four affected factors. ★ productJet22_abs_le
Elementary fourth mixed-jet bound
An ordered-hit term has at most four affected factors. Each is bounded by four, and the untouched factors are bounded by two. There are exactly card(I)^4 ordered quadruples. The proof uses only elementary finite-product and finite-sum bounds; it includes the empty set and singleton without positive-cardinality hypotheses.
theorem productJet22_abs_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
If the factor jets J of a finite index set I satisfy the factor envelopes at a point (a, u), then the mixed (2,2) jet of the finite product has absolute value at most 256·|I|⁴·2^|I|, where |I| is the number of factors.
Formal statement
hypotheses
conclusion
|productJet22 I J a u| ≤ 256 * (I.card : ℝ) ^ 4 * (2 : ℝ) ^ I.card
Proof (Lean source)
theorem productJet22_abs_le (I : Finset ι) (J : FactorJets ι) (a u : ℝ)
(h : FactorBoundsAt I J a u) :
|productJet22 I J a u| ≤
256 * (I.card : ℝ) ^ 4 * (2 : ℝ) ^ I.card := by
unfold productJet22
calc
_ ≤ ∑ i ∈ I, ∑ j ∈ I, ∑ k ∈ I, ∑ l ∈ I,
(256 * (2 : ℝ) ^ I.card) := by
refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_)
intro i hi
refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_)
intro j hj
refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_)
intro k hk
refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_)
intro l hl
exact leibnizTerm_abs_le I J [i, j] [k, l] a u h (by simp) (by simp)
_ = 256 * (I.card : ℝ) ^ 4 * (2 : ℝ) ^ I.card := by
simp only [Finset.sum_const, nsmul_eq_mul]
ring
3 supporting declarations (lemmas, instances)
-
factorJet_abs_le_fourtheorem — If the factor jets J of a finite index set I satisfy the factor envelopes at a point (a, u), then for every index i of I and all derivative orders p and q, the selected factor jet of i at orders (p, q) has absolute value at most four. The selector's zero extensions make this true at arbitrary orders.hypothesesconclusion|factorJet J i p q a u| ≤ 4Proof (Lean source)
theorem factorJet_abs_le_four (I : Finset ι) (J : FactorJets ι) (a u : ℝ) (h : FactorBoundsAt I J a u) (i : ι) (hi : i ∈ I) (p q : ℕ) : |factorJet J i p q a u| ≤ 4 := by rcases p with _ | _ | _ | p <;> rcases q with _ | _ | _ | q <;> simp only [factorJet] all_goals first | exact (h.bound00 i hi).trans (by norm_num) | exact h.bound10 i hi | exact h.bound20 i hi | exact h.bound01 i hi | exact h.bound11 i hi | exact h.bound21 i hi | exact h.bound22 i hi | norm_num -
leibnizTerm_abs_letheorem — If the factor jets J of a finite index set I satisfy the factor envelopes at a point (a, u), and a first-coordinate hit list has at most two entries and a second-coordinate hit list has at most two entries, then the corresponding ordered-hit Leibniz summand has absolute value at most 256 times two to the number of factors.hypothesesι :sharedType u_1I :Finset ιJ :xs ys :List ιa u :ℝh :FactorBoundsAt I J a uhxs :xs.length ≤ 2hys :ys.length ≤ 2conclusion|leibnizTerm I J xs ys a u| ≤ 256 * (2 : ℝ) ^ I.cardProof (Lean source)
theorem leibnizTerm_abs_le (I : Finset ι) (J : FactorJets ι) (xs ys : List ι) (a u : ℝ) (h : FactorBoundsAt I J a u) (hxs : xs.length ≤ 2) (hys : ys.length ≤ 2) : |leibnizTerm I J xs ys a u| ≤ 256 * (2 : ℝ) ^ I.card := by let T := I ∩ (xs ++ ys).toFinset have hTI : T ⊆ I := Finset.inter_subset_left have hTcard : T.card ≤ 4 := calc T.card ≤ (xs ++ ys).toFinset.card := Finset.card_le_card inter_subset_right _ ≤ (xs ++ ys).length := List.toFinset_card_le (xs ++ ys) _ ≤ 4 := by simp only [List.length_append]; omega have hT : (∏ i ∈ T, |factorJet J i (xs.count i) (ys.count i) a u|) ≤ (4 : ℝ) ^ T.card := by calc _ ≤ ∏ _i ∈ T, (4 : ℝ) := Finset.prod_le_prod (fun _ _ => abs_nonneg _) (fun i hi => factorJet_abs_le_four I J a u h i (hTI hi) _ _) _ = _ := by simp have hU : (∏ i ∈ I \ T, |factorJet J i (xs.count i) (ys.count i) a u|) ≤ (2 : ℝ) ^ (I \ T).card := by calc _ ≤ ∏ _i ∈ I \ T, (2 : ℝ) := by apply Finset.prod_le_prod (fun _ _ => abs_nonneg _) intro i hi have hiI := (Finset.mem_sdiff.mp hi).1 have hnot : i ∉ xs ∧ i ∉ ys := by simpa [T, hiI] using (Finset.mem_sdiff.mp hi).2 simpa [List.count_eq_zero_of_not_mem hnot.1, List.count_eq_zero_of_not_mem hnot.2, factorJet] using h.bound00 i hiI _ = _ := by simp calc |leibnizTerm I J xs ys a u| = (∏ i ∈ I \ T, |factorJet J i (xs.count i) (ys.count i) a u|) * (∏ i ∈ T, |factorJet J i (xs.count i) (ys.count i) a u|) := by rw [leibnizTerm, Finset.abs_prod, Finset.prod_sdiff hTI] _ ≤ (2 : ℝ) ^ (I \ T).card * (4 : ℝ) ^ T.card := mul_le_mul hU hT (Finset.prod_nonneg (fun _ _ => abs_nonneg _)) (by positivity) _ ≤ (2 : ℝ) ^ I.card * (4 : ℝ) ^ 4 := mul_le_mul (pow_le_pow_right₀ (by norm_num) (Finset.card_le_card sdiff_subset)) (pow_le_pow_right₀ (by norm_num) hTcard) (by positivity) (by positivity) _ = 256 * (2 : ℝ) ^ I.card := by norm_num; ring -
productJet22_abs_le_on_rectangletheorem — If the factor jets J of a finite index set I satisfy the factor envelopes at every point of the closed rectangle from a₀ to a₁ in the first coordinate and from u₀ to u₁ in the second, then at every point of that rectangle the mixed (2,2) jet of the finite product has absolute value at most 256·|I|⁴·2^|I|.hypothesesι :sharedType u_1I :Finset ιJ :a₀ a₁ u₀ u₁ :ℝh :∀ a ∈ Set.Icc a₀ a₁, ∀ u ∈ Set.Icc u₀ u₁, FactorBoundsAt I J a ua ∈ Set.Icc a₀ a₁ :u ∈ Set.Icc u₀ u₁ :conclusion|productJet22 I J a u| ≤ 256 * (I.card : ℝ) ^ 4 * (2 : ℝ) ^ I.cardProof (Lean source)
theorem productJet22_abs_le_on_rectangle (I : Finset ι) (J : FactorJets ι) (a₀ a₁ u₀ u₁ : ℝ) (h : ∀ a ∈ Icc a₀ a₁, ∀ u ∈ Icc u₀ u₁, FactorBoundsAt I J a u) : ∀ a ∈ Icc a₀ a₁, ∀ u ∈ Icc u₀ u₁, |productJet22 I J a u| ≤ 256 * (I.card : ℝ) ^ 4 * (2 : ℝ) ^ I.card := by intro a ha u hu exact productJet22_abs_le I J a u (h a ha u hu)
Calculus 1 core · 9 supporting The local hypotheses are exactly the supplied coordinate chains. ★ hasDerivAt_productJet21_u
Coordinate derivative certification for the explicit finite jets
The local hypotheses are exactly the supplied coordinate chains. The two elementary insertion identities and two single-summand derivative rules isolate the bookkeeping from differentiation of the outer finite sums. No higher first-coordinate derivatives or mixed-coordinate interchange theorem is used.
theorem hasDerivAt_productJet21_u reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
If the factor jets J of a finite index set I have the second-coordinate derivative chains at a point (a, u), then the mixed (2,1) jet of the finite product, as a function of the second coordinate, has derivative at u equal to the explicit mixed (2,2) jet.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem hasDerivAt_productJet21_u (I : Finset ι) (J : FactorJets ι) (a u : ℝ)
(h : UChainsAt I J a u) :
HasDerivAt (fun v => productJet21 I J a v) (productJet22 I J a u) u := by
unfold productJet21 productJet22
apply HasDerivAt.fun_sum
intro i hi
apply HasDerivAt.fun_sum
intro j hj
have hd := HasDerivAt.fun_sum (u := I) (fun k _ =>
hasDerivAt_leibnizTerm_u I J [i, j] [k] a u h (by simp) (by simp))
rw [Finset.sum_comm] at hd
exact hd
9 supporting declarations (lemmas, instances)
-
leibnizTerm_cons_atheorem — For factor jets J of a finite index set I, hit lists xs and ys and a point (a, u), if an index k belongs to I, then prepending k to the first-coordinate hit list turns the Leibniz summand into the factor jet of k with its first-coordinate order raised by one, times the unchanged jets of the other factors.hypothesesconclusionleibnizTerm I J (k :: xs) ys a uProof (Lean source)
theorem leibnizTerm_cons_a (I : Finset ι) (J : FactorJets ι) (xs ys : List ι) (k : ι) (a u : ℝ) (hk : k ∈ I) : leibnizTerm I J (k :: xs) ys a u = factorJet J k (xs.count k + 1) (ys.count k) a u * ∏ i ∈ I.erase k, factorJet J i (xs.count i) (ys.count i) a u := by unfold leibnizTerm rw [← Finset.mul_prod_erase I _ hk] simp only [List.count_cons, beq_self_eq_true, ite_true] congr 1 apply Finset.prod_congr rfl intro i hi have hne : k ≠ i := (Finset.mem_erase.mp hi).1.symm simp [hne] -
leibnizTerm_cons_utheorem — For factor jets J of a finite index set I, hit lists xs and ys and a point (a, u), if an index k belongs to I, then prepending k to the second-coordinate hit list turns the Leibniz summand into the factor jet of k with its second-coordinate order raised by one, times the unchanged jets of the other factors.hypothesesconclusionleibnizTerm I J xs (k :: ys) a uProof (Lean source)
theorem leibnizTerm_cons_u (I : Finset ι) (J : FactorJets ι) (xs ys : List ι) (k : ι) (a u : ℝ) (hk : k ∈ I) : leibnizTerm I J xs (k :: ys) a u = factorJet J k (xs.count k) (ys.count k + 1) a u * ∏ i ∈ I.erase k, factorJet J i (xs.count i) (ys.count i) a u := by unfold leibnizTerm rw [← Finset.mul_prod_erase I _ hk] simp only [List.count_cons, beq_self_eq_true, ite_true] congr 1 apply Finset.prod_congr rfl intro i hi have hne : k ≠ i := (Finset.mem_erase.mp hi).1.symm simp [hne] -
hasDerivAt_factorJet_atheorem — If the factor jets J of a finite index set I have the first-coordinate derivative chains at a point (a, u), then for every index i of I and every first-coordinate order p at most one, the factor jet of i at orders (p, 0), as a function of the first coordinate, has derivative at a equal to its jet at orders (p + 1, 0).hypothesesι :sharedType u_1I :Finset ιJ :a u :ℝh :AChainsAt I J a ui :ιhi :i ∈ Ip :ℕhp :p ≤ 1conclusionProof (Lean source)
theorem hasDerivAt_factorJet_a (I : Finset ι) (J : FactorJets ι) (a u : ℝ) (h : AChainsAt I J a u) (i : ι) (hi : i ∈ I) (p : ℕ) (hp : p ≤ 1) : HasDerivAt (fun b => factorJet J i p 0 b u) (factorJet J i (p + 1) 0 a u) a := by obtain rfl | rfl : p = 0 ∨ p = 1 := by omega · exact h.da00 i hi · exact h.da10 i hi -
hasDerivAt_factorJet_utheorem — If the factor jets J of a finite index set I have the second-coordinate derivative chains at a point (a, u), then for every index i of I and orders p and q with p at most two and q at most one, the factor jet of i at orders (p, q), as a function of the second coordinate, has derivative at u equal to its jet at orders (p, q + 1).hypothesesι :sharedType u_1I :Finset ιJ :a u :ℝh :UChainsAt I J a ui :ιhi :i ∈ Ip q :ℕhp :p ≤ 2hq :q ≤ 1conclusionProof (Lean source)
theorem hasDerivAt_factorJet_u (I : Finset ι) (J : FactorJets ι) (a u : ℝ) (h : UChainsAt I J a u) (i : ι) (hi : i ∈ I) (p q : ℕ) (hp : p ≤ 2) (hq : q ≤ 1) : HasDerivAt (fun v => factorJet J i p q a v) (factorJet J i p (q + 1) a u) u := by obtain rfl | rfl | rfl : p = 0 ∨ p = 1 ∨ p = 2 := by omega · obtain rfl | rfl : q = 0 ∨ q = 1 := by omega · exact h.du00 i hi · exact h.du01 i hi · obtain rfl | rfl : q = 0 ∨ q = 1 := by omega · exact h.du10 i hi · exact h.du11 i hi · obtain rfl | rfl : q = 0 ∨ q = 1 := by omega · exact h.du20 i hi · exact h.du21 i hi -
hasDerivAt_leibnizTerm_atheorem — If the factor jets J of a finite index set I have the first-coordinate derivative chains at a point (a, u) and a first-coordinate hit list xs has at most one entry, then the Leibniz summand with hits xs and no second-coordinate hits, as a function of the first coordinate, has derivative at a equal to the sum over k in I of the summand with k prepended to xs.hypothesesconclusionProof (Lean source)
theorem hasDerivAt_leibnizTerm_a (I : Finset ι) (J : FactorJets ι) (xs : List ι) (a u : ℝ) (h : AChainsAt I J a u) (hlen : xs.length ≤ 1) : HasDerivAt (fun b => leibnizTerm I J xs [] b u) (∑ k ∈ I, leibnizTerm I J (k :: xs) [] a u) a := by have hd := HasDerivAt.fun_finsetProd (fun i hi => hasDerivAt_factorJet_a I J a u h i hi (xs.count i) ((List.count_le_length).trans hlen)) have hs : (∑ k ∈ I, leibnizTerm I J (k :: xs) [] a u) = ∑ k ∈ I, (∏ i ∈ I.erase k, factorJet J i (xs.count i) 0 a u) • factorJet J k (xs.count k + 1) 0 a u := by apply Finset.sum_congr rfl intro k hk rw [leibnizTerm_cons_a I J xs [] k a u hk] simp only [List.count_nil, smul_eq_mul, mul_comm] rw [← hs] at hd exact hd -
hasDerivAt_leibnizTerm_utheorem — If the factor jets J of a finite index set I have the second-coordinate derivative chains at a point (a, u), and a first-coordinate hit list has at most two entries and a second-coordinate hit list has at most one entry, then the Leibniz summand, as a function of the second coordinate, has derivative at u equal to the sum over k in I of the summand with k prepended to the second-coordinate list.hypothesesι :sharedType u_1I :Finset ιJ :xs ys :List ιa u :ℝh :UChainsAt I J a uhxs :xs.length ≤ 2hys :ys.length ≤ 1conclusionProof (Lean source)
theorem hasDerivAt_leibnizTerm_u (I : Finset ι) (J : FactorJets ι) (xs ys : List ι) (a u : ℝ) (h : UChainsAt I J a u) (hxs : xs.length ≤ 2) (hys : ys.length ≤ 1) : HasDerivAt (fun v => leibnizTerm I J xs ys a v) (∑ k ∈ I, leibnizTerm I J xs (k :: ys) a u) u := by have hd := HasDerivAt.fun_finsetProd (fun i hi => hasDerivAt_factorJet_u I J a u h i hi (xs.count i) (ys.count i) ((List.count_le_length).trans hxs) ((List.count_le_length).trans hys)) have hs : (∑ k ∈ I, leibnizTerm I J xs (k :: ys) a u) = ∑ k ∈ I, (∏ i ∈ I.erase k, factorJet J i (xs.count i) (ys.count i) a u) • factorJet J k (xs.count k) (ys.count k + 1) a u := by apply Finset.sum_congr rfl intro k hk rw [leibnizTerm_cons_u I J xs ys k a u hk] simp only [smul_eq_mul, mul_comm] rw [← hs] at hd exact hd -
hasDerivAt_product_atheorem — If the factor jets J of a finite index set I have the first-coordinate derivative chains at a point (a, u), then the finite product of the base factors, as a function of the first coordinate, has derivative at a equal to the explicit first first-coordinate jet.hypothesesconclusionProof (Lean source)
theorem hasDerivAt_product_a (I : Finset ι) (J : FactorJets ι) (a u : ℝ) (h : AChainsAt I J a u) : HasDerivAt (fun b => product I J b u) (productJet10 I J a u) a := by simpa only [product, productJet10, leibnizTerm, List.count_nil, factorJet] using hasDerivAt_leibnizTerm_a I J [] a u h (by simp) -
hasDerivAt_productJet10_atheorem — If the factor jets J of a finite index set I have the first-coordinate derivative chains at a point (a, u), then the first first-coordinate jet of the finite product, as a function of the first coordinate, has derivative at a equal to the explicit second first-coordinate jet.hypothesesconclusionProof (Lean source)
theorem hasDerivAt_productJet10_a (I : Finset ι) (J : FactorJets ι) (a u : ℝ) (h : AChainsAt I J a u) : HasDerivAt (fun b => productJet10 I J b u) (productJet20 I J a u) a := by have hd := HasDerivAt.fun_sum (u := I) (fun i _ => hasDerivAt_leibnizTerm_a I J [i] a u h (by simp)) rw [Finset.sum_comm] at hd exact hd -
hasDerivAt_productJet20_utheorem — If the factor jets J of a finite index set I have the second-coordinate derivative chains at a point (a, u), then the second first-coordinate jet of the finite product, as a function of the second coordinate, has derivative at u equal to the explicit mixed (2,1) jet.hypothesesconclusionProof (Lean source)
theorem hasDerivAt_productJet20_u (I : Finset ι) (J : FactorJets ι) (a u : ℝ) (h : UChainsAt I J a u) : HasDerivAt (fun v => productJet20 I J a v) (productJet21 I J a u) u := by exact HasDerivAt.fun_sum (u := I) (fun i _ => HasDerivAt.fun_sum (u := I) (fun j _ => hasDerivAt_leibnizTerm_u I J [i, j] [] a u h (by simp) (by simp)))
Support 2 core · 8 supporting The second-coordinate support is the set of hit indices, while the occurrence count retains the order at each index. ★ productJet22_support_decomposition
Support-visible finite Leibniz expansions
The second-coordinate support is the set of hit indices, while the occurrence count retains the order at each index. The total order is two for every (2,2) summand. The expansion separates a single factor's (2,2) jet from two distinct factors with positive second-coordinate order. A companion expansion displays the familiar diagonal and off-diagonal formula for the (2,0) jet.
def secondSupport reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The second-coordinate derivative support of a hit list is its set of distinct indices. The list, rather than this set alone, retains the order at each index.
theorem productJet22_support_decomposition reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Calculus.FiniteProduct
The explicit mixed (2,2) jet of the finite product of the factors J over the index set I at a point (a, u) equals the sum, over single factors, of that factor's (2,2) jet times the base values of all the other factors, plus the sum of the ordered-hit Leibniz summands over all ordered pairs of first-coordinate hits and all ordered pairs of two distinct second-coordinate hits.
Formal statement
hypotheses
conclusion
productJet22 I J a u
= (∑ r ∈ I, J.f22 r a u * ∏ i ∈ I.erase r, J.f00 i a u)
+ ∑ p ∈ I, ∑ q ∈ I, ∑ r ∈ I, ∑ s ∈ I.erase r, leibnizTerm I J [p, q] [r, s] a u
Proof (Lean source)
theorem productJet22_support_decomposition (I : Finset ι) (J : FactorJets ι)
(a u : ℝ) :
productJet22 I J a u =
(∑ r ∈ I, J.f22 r a u * ∏ i ∈ I.erase r, J.f00 i a u) +
∑ p ∈ I, ∑ q ∈ I, ∑ r ∈ I, ∑ s ∈ I.erase r,
leibnizTerm I J [p, q] [r, s] a u := by
unfold productJet22
calc
_ = (∑ p ∈ I, ∑ q ∈ I, ∑ r ∈ I,
leibnizTerm I J [p, q] [r, r] a u) +
∑ p ∈ I, ∑ q ∈ I, ∑ r ∈ I, ∑ s ∈ I.erase r,
leibnizTerm I J [p, q] [r, s] a u := by
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro p hp
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro q hq
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro r hr
exact (Finset.add_sum_erase I _ hr).symm
_ = _ := by
congr 1
calc
_ = ∑ r ∈ I, ∑ p ∈ I, ∑ q ∈ I,
leibnizTerm I J [p, q] [r, r] a u := by
calc
_ = ∑ p ∈ I, ∑ r ∈ I, ∑ q ∈ I,
leibnizTerm I J [p, q] [r, r] a u := by
apply Finset.sum_congr rfl
intro p hp
rw [Finset.sum_comm]
_ = _ := Finset.sum_comm
_ = _ := by
apply Finset.sum_congr rfl
intro r hr
rw [Finset.sum_eq_single r]
· rw [Finset.sum_eq_single r]
· exact leibnizTerm22_all_same I J r a u hr
· intro q hq hqr
exact leibnizTerm22_repeated_u_zero I J r q r a u hr (inr hqr)
· exact fun h => (h hr).elim
· intro p hp hpr
apply Finset.sum_eq_zero
intro q hq
exact leibnizTerm22_repeated_u_zero I J p q r a u hr (inl hpr)
· exact fun h => (h hr).elim
8 supporting declarations (lemmas, instances)
-
mem_secondSupport_ifftheorem — An index lies in the second-coordinate support exactly when its derivative order is positive.Proof (Lean source)
theorem mem_secondSupport_iff (ys : List ι) (i : ι) : i ∈ secondSupport ys ↔ 0 < ys.count i := by simpa only [secondSupport, List.mem_toFinset] using (List.count_pos_iff (a := i) (l := ys)).symm -
sum_second_orderstheorem — If every entry of a hit list ys lies in a finite index set I, then the number of occurrences of each index of I in ys, summed over I, equals the length of ys.hypothesesconclusion∑ i ∈ I, ys.count i = ys.lengthProof (Lean source)
theorem sum_second_orders (I : Finset ι) (ys : List ι) (hys : ∀ i ∈ ys, i ∈ I) : ∑ i ∈ I, ys.count i = ys.length := by induction ys with | nil => simp | cons r ys ih => have hr : r ∈ I := hys r (by simp) have htail : ∀ i ∈ ys, i ∈ I := fun i hi => hys i (by simp [hi]) simp only [List.count_cons, List.length_cons, Finset.sum_add_distrib, ih htail] simp only [beq_iff_eq, Finset.sum_ite_eq, hr, ite_true] -
summand22_total_second_ordertheorem — If two second-coordinate hits r and s both lie in a finite index set I, then the occurrence counts of the indices of I in the two-element hit list r, s sum to two, including when r and s are equal.hypothesesconclusion∑ i ∈ I, ([r, s] : List ι).count i = 2Proof (Lean source)
theorem summand22_total_second_order (I : Finset ι) (r s : ι) (hr : r ∈ I) (hs : s ∈ I) : ∑ i ∈ I, ([r, s] : List ι).count i = 2 := by simpa using sum_second_orders I [r, s] (by intro i hi simp only [List.mem_cons, List.not_mem_nil, or_false] at hi rcases hi with rfl | rfl <;> assumption) -
secondSupport_pairtheorem — The support of two second-coordinate hits is precisely the pair of hit indices; equal hits give a singleton.Proof (Lean source)
-
productJet20_eq_diagonal_add_offDiagonaltheorem — The explicit (2,0) jet equals the diagonal sum of second factor jets plus the ordered distinct-index sum of products of first factor jets. Thus both first-coordinate Leibniz cases are exposed.hypothesesconclusionproductJet20 I J a u= (∑ i ∈ I, J.f20 i a u * ∏ k ∈ I.erase i, J.f00 k a u)+ ∑ i ∈ I, ∑ j ∈ I.erase i, J.f10 i a u * J.f10 j a u * ∏ k ∈ (I.erase i).erase j, J.f00 k a uProof (Lean source)
theorem productJet20_eq_diagonal_add_offDiagonal (I : Finset ι) (J : FactorJets ι) (a u : ℝ) : productJet20 I J a u = (∑ i ∈ I, J.f20 i a u * ∏ k ∈ I.erase i, J.f00 k a u) + ∑ i ∈ I, ∑ j ∈ I.erase i, J.f10 i a u * J.f10 j a u * ∏ k ∈ (I.erase i).erase j, J.f00 k a u := by unfold productJet20 rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi rw [← Finset.add_sum_erase I _ hi] congr 1 · unfold leibnizTerm rw [← Finset.mul_prod_erase I _ hi] simp only [List.count_cons, List.count_nil, beq_self_eq_true, ite_true, factorJet] congr 1 apply Finset.prod_congr rfl intro k hk have hik : i ≠ k := (Finset.mem_erase.mp hk).1.symm simp [hik] · apply Finset.sum_congr rfl intro j hj have hji : j ≠ i := (Finset.mem_erase.mp hj).1 unfold leibnizTerm rw [← Finset.mul_prod_erase I _ hi, ← Finset.mul_prod_erase (I.erase i) _ hj] simp only [List.count_cons, List.count_nil, beq_self_eq_true, ite_true, beq_iff_eq, hji, hji.symm, ite_false, factorJet] rw [← mul_assoc] congr 1 apply Finset.prod_congr rfl intro k hk have hjk : j ≠ k := (Finset.mem_erase.mp hk).1.symm have hik : i ≠ k := (Finset.mem_erase.mp (Finset.mem_erase.mp hk).2).1.symm simp [hik, hjk] -
leibnizTerm22_repeated_u_zerotheorem — For factor jets J of a finite index set I at a point (a, u), if an index r of I is hit twice in the second coordinate and the two first-coordinate hits p and q are not both r, then the corresponding (2,2) Leibniz summand is zero.hypothesesconclusionleibnizTerm I J [p, q] [r, r] a u = 0Proof (Lean source)
theorem leibnizTerm22_repeated_u_zero (I : Finset ι) (J : FactorJets ι) (p q r : ι) (a u : ℝ) (hr : r ∈ I) (hnot : p ≠ r ∨ q ≠ r) : leibnizTerm I J [p, q] [r, r] a u = 0 := by unfold leibnizTerm rw [← Finset.mul_prod_erase I _ hr] have hz : factorJet J r (([p, q] : List ι).count r) 2 a u = 0 := by rcases hnot with hp | hq · by_cases hq : q = r <;> simp [hp, hq, factorJet] · by_cases hp : p = r <;> simp [hp, hq, factorJet] simpa using congrArg (fun x : ℝ => x * ∏ i ∈ I.erase r, factorJet J i (([p, q] : List ι).count i) (([r, r] : List ι).count i) a u) hz -
leibnizTerm22_all_sametheorem — For factor jets J of a finite index set I at a point (a, u), if all four hits fall on one index r of I, then the Leibniz summand equals the (2,2) jet of r times the product of the base factors of the other indices.hypothesesconclusionleibnizTerm I J [r, r] [r, r] a u = J.f22 r a u * ∏ i ∈ I.erase r, J.f00 i a uProof (Lean source)
theorem leibnizTerm22_all_same (I : Finset ι) (J : FactorJets ι) (r : ι) (a u : ℝ) (hr : r ∈ I) : leibnizTerm I J [r, r] [r, r] a u = J.f22 r a u * ∏ i ∈ I.erase r, J.f00 i a u := by unfold leibnizTerm rw [← Finset.mul_prod_erase I _ hr] simp only [List.count_cons, List.count_nil, beq_self_eq_true, ite_true, factorJet] congr 1 apply Finset.prod_congr rfl intro i hi have hri : r ≠ i := (Finset.mem_erase.mp hi).1.symm simp [hri] -
leibnizTerm22_vanishes_outsidetheorem — For factor jets J of a finite index set I at a point (a, u) and first-coordinate hits p and q, suppose the second-coordinate hits r and s lie in I, every factor of I outside a set M has vanishing (0,1), (1,1), (2,1) and (2,2) jets, and r or s lies outside M. Then the corresponding (2,2) Leibniz summand is zero.hypothesesι :sharedType u_1I M :Finset ιJ :p q r s :ιa u :ℝhr :r ∈ Ihs :s ∈ Ihzero :∀ i ∈ Iifi ∉ MthenJ.f01 i a u = 0 ∧ J.f11 i a u = 0 ∧ J.f21 i a u = 0 ∧ J.f22 i a u = 0houtside :r ∉ M ∨ s ∉ MconclusionleibnizTerm I J [p, q] [r, s] a u = 0Proof (Lean source)
theorem leibnizTerm22_vanishes_outside (I M : Finset ι) (J : FactorJets ι) (p q r s : ι) (a u : ℝ) (hr : r ∈ I) (hs : s ∈ I) (hzero : ∀ i ∈ I, i ∉ M → J.f01 i a u = 0 ∧ J.f11 i a u = 0 ∧ J.f21 i a u = 0 ∧ J.f22 i a u = 0) (houtside : r ∉ M ∨ s ∉ M) : leibnizTerm I J [p, q] [r, s] a u = 0 := by obtain ⟨t, ht, htm, hhit⟩ : ∃ t ∈ I, t ∉ M ∧ (r = t ∨ s = t) := by rcases houtside with hrm | hsm · exact ⟨r, hr, hrm, inl rfl⟩ · exact ⟨s, hs, hsm, inr rfl⟩ obtain ⟨h01, h11, h21, h22⟩ := hzero t ht htm unfold leibnizTerm rw [← Finset.mul_prod_erase I _ ht] have hz : factorJet J t (([p, q] : List ι).count t) (([r, s] : List ι).count t) a u = 0 := by rcases hhit with hr | hs · subst r by_cases hp : p = t <;> by_cases hq : q = t <;> by_cases hs : s = t <;> simp [hp, hq, hs, factorJet, h01, h11, h21, h22] · subst s by_cases hp : p = t <;> by_cases hq : q = t <;> by_cases hr : r = t <;> simp [hp, hq, hr, factorJet, h01, h11, h21, h22] rw [hz, zero_mul]