Grace/Cumulus/Complex/ExtremeValue.g17

Open in Workbench Download source

Imports

SequentialContinuity · Real.Analysis.ExtremeValue

Declarations

Source

1-- Minimum attainment for continuous complex functions on compact sets.2-- The image-selection and real extreme-value route here uses Global Choice.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Complex.ExtremeValue9import SequentialContinuity10import Real.Analysis.ExtremeValue1112def complexNormImage (f S : Set) : Set := { complexNormSquared(f(z)) | z ∈ S }1314theorem complexNormImage.subset_reals (f S : Set)15  requires function : f : complexCarrier → complexCarrier16  requires subset : S ⊆ complexCarrier17  shows complexNormImage(f, S) ⊆ ℝ18proof19  intros t member20  obtain ⟨z, zIn, value⟩ := complexNormImage.membership.forward with member21  have zComplex := subset with z, zIn22  have image := FunctionBetween.apply_closed with *23  have typed : complexNormSquared(f(z)) ∈ ℝ by typecheck24  rwa value at typed2526defchoose complexNormPreimage (f S u : Set, n : Nat) (z ∈ complexCarrier) :=27  z ∈ S ∧ complexNormSquared(f(z)) = u(n)28requires subset : S ⊆ complexCarrier29requires terms : TermsIn(u, complexNormImage(f, S))30proof31  have nIn : n ∈ ℕ by typecheck32  have term := terms with n, nIn33  obtain ⟨z, zIn, value⟩ := complexNormImage.membership.forward at f, S, u(n) with *34  have member := subset with z, zIn35  refine ⟨z, member, zIn, value⟩3637defgraph complexNormPreimages (f S u : Set) (n ∈ ℕ) : complexCarrier := complexNormPreimage(f, S, u, n)38requires subset : S ⊆ complexCarrier39requires terms : TermsIn(u, complexNormImage(f, S))40proof41  have chosen := complexNormPreimage.selected at f, S, u, n with *42  exact chosen.left4344theorem complexNormPreimages.properties (f S u : Set) (n : Nat)45  requires subset : S ⊆ complexCarrier46  requires terms : TermsIn(u, complexNormImage(f, S))47  shows complexNormPreimages(f, S, u)(n) ∈ S ∧ complexNormSquared(f(complexNormPreimages(f, S, u)(n))) = u(n)48proof49  have chosen := complexNormPreimage.selected at f, S, u, n with *50  rw complexNormPreimages.value51  exact chosen.right5253theorem complexNormPreimages.terms (f S u : Set)54  requires subset : S ⊆ complexCarrier55  requires terms : TermsIn(u, complexNormImage(f, S))56  shows TermsIn(complexNormPreimages(f, S, u), S)57proof58  intros n member59  have natural := nat.omega.backward at n with *60  have chosen := complexNormPreimages.properties with *61  exact chosen.left6263theorem complexNormImage.sequentially_compact (f S : Set)64  requires continuous : ComplexContinuous(f)65  requires compact : ComplexSequentiallyCompact(S)66  shows SequentiallyCompact(complexNormImage(f, S))67proof68  rcases continuous with ⟨function, atPoints⟩69  rcases compact with ⟨subset, extract⟩70  have imageSubset := complexNormImage.subset_reals with *71  unfold SequentiallyCompact72  refine ⟨imageSubset, ?_⟩73  intros u sequence terms74  have preimageSequence : ComplexSequence(complexNormPreimages(f, S, u))75    unfold ComplexSequence76    exact complexNormPreimages.function at f, S, u with *77  have preimageTerms := complexNormPreimages.terms with *78  obtain ⟨k, increasing, a, aIn, converges⟩ := extract with complexNormPreimages(f, S, u), preimageSequence, preimageTerms79  have aComplex : a ∈ complexCarrier by exact subset with a, aIn80  have local := atPoints with a, aComplex81  have mapped := ComplexContinuousAt.converges with *82  have normLimit := ComplexConvergesTo.norm_squared with converges83  have selected := subsequence.sequence with *84  have selectedPreimages := complexSubsequence.sequence with *85  have mappedSequence := complexMappedSequence.sequence at f, complexSubsequence(complexNormPreimages(f, S, u), k) with *86  have image := FunctionBetween.apply_closed with *87  have same : ∀ n ∈ ℕ, subsequence(u, k)(n) = complexNormSequence(complexMappedSequence(f, complexSubsequence(complexNormPreimages(f, S, u), k)))(n)88    intros n nIn89    have natural := nat.omega.backward at n with *90    have selector := StrictlyIncreasingNat.function with increasing91    have kn := FunctionBetween.apply_closed at k, ℕ, ℕ, n with *92    have knNat := nat.omega.backward at k(n) with *93    have chosen := complexNormPreimages.properties at f, S, u, k(n) with *94    rw [complexNormSequence.value, complexMappedSequence.value, complexSubsequence.value, subsequence.value]95    symm96    exact chosen.right97  have outputLimit := ConvergesTo.of_equal_terms at subsequence(u, k), complexNormSequence(complexMappedSequence(f, complexSubsequence(complexNormPreimages(f, S, u), k))), complexNormSquared(f(a)) with *98  have imageMember : complexNormSquared(f(a)) ∈ complexNormImage(f, S)99    exact complexNormImage.membership.backward with ⟨a, aIn, rfl⟩100  have normIn : complexNormSquared(f(a)) ∈ ℝ by typecheck101  refine ⟨k, increasing, complexNormSquared(f(a)), normIn, imageMember, outputLimit⟩102103theorem ComplexContinuous.minimum_on_compact (f S : Set)104  requires continuous : ComplexContinuous(f)105  requires compact : ComplexSequentiallyCompact(S)106  requires inhabited : Nonempty(S)107  shows ∃ a ∈ S, ∀ z ∈ S, complexNormSquared(f(a)) ≤ complexNormSquared(f(z))108proof109  have imageCompact := complexNormImage.sequentially_compact with *110  have imageInhabited : Nonempty(complexNormImage(f, S))111    obtain ⟨z, member⟩ := inhabited112    witness complexNormSquared(f(z))113    exact complexNormImage.membership.backward with ⟨z, member, rfl⟩114  obtain ⟨t, tIn, least⟩ := SequentiallyCompact.has_minimum at complexNormImage(f, S) with *115  obtain ⟨a, aIn, value⟩ := complexNormImage.membership.forward at f, S, t with *116  refine ⟨a, aIn, ?_⟩117  intros z zIn118  have imageMember : complexNormSquared(f(z)) ∈ complexNormImage(f, S)119    exact complexNormImage.membership.backward with ⟨z, zIn, rfl⟩120  have bound := least with complexNormSquared(f(z)), imageMember121  rwa value122123theorem closedComplexDisk.nonempty (radius : Real)124  requires nonnegative : realZero ≤ radius125  shows Nonempty(closedComplexDisk(radius))126proof127  witness complexZero128  apply closedComplexDisk.membership.backward129  constructor130  . exact complexZero.member131  . rw complexNormSquared.zero132    exact nonnegative133134theorem complexPolynomial.disk_minimum (cs : List(complexCarrier)) (radius : Real)135  requires nonnegative : realZero ≤ radius136  shows ComplexDiskMinimum(complexPolynomial(cs), radius)137proof138  have continuous := complexPolynomial.continuous with *139  have compact := closedComplexDisk.sequentially_compact with *140  have inhabited := closedComplexDisk.nonempty with *141  obtain ⟨a, aIn, least⟩ := ComplexContinuous.minimum_on_compact at complexPolynomial(cs), closedComplexDisk(radius) with *142  have disk := closedComplexDisk.membership.forward with aIn143  unfold ComplexDiskMinimum144  refine ⟨a, disk.left, disk.right, ?_⟩145  intros z zIn bound146  have member : z ∈ closedComplexDisk(radius)147    apply closedComplexDisk.membership.backward148    refine ⟨zIn, bound⟩149  exact least with z, member150151theorem complexPolynomial.global_minimum (c : Set) (cs : List(complexCarrier))152  requires coefficient : c ∈ complexCarrier153  shows ∃ a ∈ complexCarrier, ∀ z ∈ complexCarrier, complexNormSquared(complexPolynomial(c :: cs)(a)) ≤ complexNormSquared(complexPolynomial(c :: cs)(z))154proof155  have disks : ∀ radius ∈ ℝ, realZero ≤ radius → ComplexDiskMinimum(complexPolynomial(c :: cs), radius)156    intros radius realRadius nonnegative157    exact complexPolynomial.disk_minimum with *158  exact complexPolynomial.minimum_of_disk_minima with *159160section Complexes161notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)162163theorem complexPolynomial.root_of_descent (c : Set) (cs : List(ℂ))164  requires coefficient : c ∈ ℂ165  requires descent : ∀ a ∈ ℂ, complexPolynomial(c :: cs)(a) ≠ ℂ[0] → ∃ z ∈ ℂ, complexNormSquared(complexPolynomial(c :: cs)(z)) < complexNormSquared(complexPolynomial(c :: cs)(a))166  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, c :: cs) = ℂ[0]167proof168  have minimum := complexPolynomial.global_minimum with *169  exact complexPolynomial.root_of_minimum_and_descent with *170171end Complexes172