OAI/Geometry/HarmonicGrowth/Attainment.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HarmonicCounterexample.Transmission.robust_zero line 14

   Source documentation

   The robust local attainment argument, with constants independent of the preceding pulse history. This is a genuine zero, not an approximate inverse.

   theorem robust_zero {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       [CompleteSpace E] (f : E → E) (f' : E → E →L[ℝ] E)
       (A : E ≃L[ℝ] E) {r : ℝ} (hr : 0 < r)
       (hderiv : ∀ x ∈ Metric.closedBall (0 : E) r, HasFDerivAt f (f' x) x)
       (hbound : ∀ x ∈ Metric.closedBall (0 : E) r,
         ‖ContinuousLinearMap.id ℝ E - A.symm.toContinuousLinearMap.comp (f' x)‖ ≤ 1 / 2)
       (hstart : ‖A.symm (f 0)‖ ≤ r / 2) :
       ∃ x ∈ Metric.closedBall (0 : E) r, f x = 0 := by
   …

2. abbrev OAI.HarmonicCounterexample.FiniteControl.MatrixProduct' line 80
3. def OAI.HarmonicCounterexample.FiniteControl.tracefreeProduct' line 82
4. def OAI.HarmonicCounterexample.FiniteControl.meanTrace line 88
5. def OAI.HarmonicCounterexample.FiniteControl.tracefreeProjection line 93

   Source documentation

   Linear local SL chart: project away scalar matrices after translating the exact target to the identity. No abstract manifold chart is assumed.

   def tracefreeProjection : MatrixProduct' (ι:=ι) →ₗ[ℝ] tracefreeProduct' (ι:=ι) where
   …

   Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct', OAI.HarmonicCounterexample.FiniteControl.tracefreeProduct'

6. lemma OAI.HarmonicCounterexample.FiniteControl.tracefreeProjection_zero_iff line 114

   Source documentation

   Projection zero is exactly scalarity, with the scalar given explicitly.

   lemma tracefreeProjection_zero_iff (X : MatrixProduct' (ι:=ι)) :
   …

   Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'

7. lemma OAI.HarmonicCounterexample.FiniteControl.tracefreeProjection_id line 126
8. lemma OAI.HarmonicCounterexample.FiniteControl.tracefreeProjection_subtype line 132
9. lemma OAI.HarmonicCounterexample.FiniteControl.positive_scalar_of_projection_zero line 141

   Source documentation

   Positivity of trace resolves the spurious negative scalar branch. This is an OPEN condition near the prescribed positive scalar times the target.

   lemma positive_scalar_of_projection_zero {X : MatrixProduct' (ι:=ι)}
   …

   Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'

10. lemma OAI.HarmonicCounterexample.FiniteControl.exact_scalar_target line 150

    Source documentation

    Vanishing projected transmission gives the EXACT target, up to the positive scalar permitted by source equation (exact-transmission).

    lemma exact_scalar_target {X : MatrixProduct' (ι:=ι)} (M : (MatrixProduct' (ι:=ι))ˣ)
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'

11. theorem OAI.HarmonicCounterexample.Transmission.robust_zero_of_comparison line 178

    Source documentation

    The manuscript's two quarter bounds imply its half contraction, without any implicit inverse-function robustness assertion.

    theorem robust_zero_of_comparison (f : E → E) (f' g' : E → E →L[ℝ] E)
        (A : E ≃L[ℝ] E) {r : ℝ} (hr : 0 < r)
        (hderiv : ∀ x ∈ Metric.closedBall (0:E) r,HasFDerivAt f (f' x) x)
        (hbase : ∀ x ∈ Metric.closedBall (0:E) r,
          ‖ContinuousLinearMap.id ℝ E-A.symm.toContinuousLinearMap.comp (g' x)‖ ≤ 1/4)
        (herr : ∀ x ∈ Metric.closedBall (0:E) r,
          ‖A.symm.toContinuousLinearMap.comp (f' x-g' x)‖ ≤ 1/4)
        (hstart : ‖A.symm (f 0)‖ ≤ r/2) :
        ∃ x ∈ Metric.closedBall (0:E) r,f x=0 := by
    …

12. theorem OAI.HarmonicCounterexample.Transmission.comparison_ball line 213

    Source documentation

    A single comparison ball is selected from the finite control word, before any history or period is given. Continuity of its derivative is sufficient.

    theorem comparison_ball (g' : E → E →L[ℝ] E) (A : E ≃L[ℝ] E)
        (hc : ContinuousAt g' 0) (h0 : g' 0=A.toContinuousLinearMap) :
        ∃ r : ℝ,0 < r ∧ ∀ x ∈ Metric.closedBall (0:E) r,
          ‖ContinuousLinearMap.id ℝ E-A.symm.toContinuousLinearMap.comp (g' x)‖ ≤ 1/4 := by
    …

13. theorem OAI.HarmonicCounterexample.Transmission.uniform_attainment_tolerance line 233

    Source documentation

    Quantitative uniform local attainment: the only family-specific inputs are C1 errors of actual maps against a fixed regular control word. The same radius and epsilon work for all preceding histories.

    theorem uniform_attainment_tolerance (g : E → E) (g' : E → E →L[ℝ] E)
        (A : E ≃L[ℝ] E) (hg0 : g 0=0) (hgc : ContinuousAt g' 0)
        (hg'0 : g' 0=A.toContinuousLinearMap) :
        ∃ r ε : ℝ,0 < r ∧ 0 < ε ∧
          ∀ (f : E → E) (f' : E → E →L[ℝ] E),
            (∀ x ∈ Metric.closedBall (0:E) r,HasFDerivAt f (f' x) x) →
            ‖f 0-g 0‖ ≤ ε →
            (∀ x ∈ Metric.closedBall (0:E) r,‖f' x-g' x‖ ≤ ε) →
            ∃ x ∈ Metric.closedBall (0:E) r,f x=0 := by
    …

14. theorem OAI.HarmonicCounterexample.Transmission.uniform_projected_attainment line 284

    Source documentation

    The fixed local chart radius and C1 tolerance are selected BEFORE any actual history-dependent map. The attained point stays in any prescribed open neighborhood of the target, in particular the positive-trace branch.

    theorem uniform_projected_attainment
        (Φ : E → F) (Φ' : E → E →L[ℝ] F) (L : F →L[ℝ] E) (A : E ≃L[ℝ] E)
        (hΦ : ContinuousAt Φ 0) (hΦ' : ContinuousAt Φ' 0)
        (hzero : L (Φ 0)=0) (hjet : L.comp (Φ' 0)=A.toContinuousLinearMap)
        {U : Set F} (hU : IsOpen U) (htgt : Φ 0 ∈ U) :
        ∃ r ε : ℝ,0 < r ∧ 0 < ε ∧
          ∀ (Ψ : E → F) (Ψ' : E → E →L[ℝ] F),
            (∀ x ∈ Metric.closedBall (0:E) r,HasFDerivAt Ψ (Ψ' x) x) →
            (∀ x ∈ Metric.closedBall (0:E) r,‖Ψ x-Φ x‖ ≤ ε) →
            (∀ x ∈ Metric.closedBall (0:E) r,‖Ψ' x-Φ' x‖ ≤ ε) →
            ∃ x ∈ Metric.closedBall (0:E) r,L (Ψ x)=0 ∧ Ψ x ∈ U := by
    …

15. def OAI.HarmonicCounterexample.FiniteControl.translatedProjection line 373
16. lemma OAI.HarmonicCounterexample.FiniteControl.translatedProjection_apply line 378
17. lemma OAI.HarmonicCounterexample.FiniteControl.positive_trace_neighborhood line 382
18. theorem OAI.HarmonicCounterexample.FiniteControl.uniform_exact_scalar_attainment line 412

    Source documentation

    Quantitative actual exact positive-scalar attainment, avoiding determinant normalization altogether. Each actual map has genuine Frechet derivatives and uniform C1 errors; the same tolerance works for every preceding history.

    theorem uniform_exact_scalar_attainment
        (M : (MatrixProduct' (ι:=ι))ˣ) (Φ : E → MatrixProduct' (ι:=ι))
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'

19. def OAI.HarmonicCounterexample.FiniteControl.boundedScalarNeighborhood line 461
20. lemma OAI.HarmonicCounterexample.FiniteControl.boundedScalarNeighborhood_open line 464
21. lemma OAI.HarmonicCounterexample.FiniteControl.bounded_scalar_target line 482
22. theorem OAI.HarmonicCounterexample.FiniteControl.uniform_exact_bounded_scalar_attainment line 502

    Source documentation

    The exact target scalar stays in a fixed compact positive range. This also supplies the uniform logarithmic scalar bound required for growth.

    theorem uniform_exact_bounded_scalar_attainment
        (M : (MatrixProduct' (ι:=ι))ˣ) (Φ : E → MatrixProduct' (ι:=ι))
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'

23. lemma OAI.HarmonicCounterexample.Transmission.full_leg_factor line 552

    Source documentation

    Factoring the entire diagonal leg; unlike factoring only the dwell, no large diagonal anisotropy is left inside the error term. Multiplication order is the literal source order D * permutation.

    lemma full_leg_factor (U V P B : R) (θ : ℝ) (D : Rˣ)
        (hD : (D:R)=U+θ • V) :
        (↑D⁻¹:R)*((U+V*P)*B)=
          (1+((↑D⁻¹:R)*V)*(P-θ • (1:R)))*B := by
    …

24. def OAI.HarmonicCounterexample.Transmission.wholePeriod line 562
25. def OAI.HarmonicCounterexample.Transmission.wholePeriodJet line 564
26. lemma OAI.HarmonicCounterexample.Transmission.wholePeriodJet_apply line 570
27. lemma OAI.HarmonicCounterexample.Transmission.wholePeriod_hasFDerivAt line 574
28. lemma OAI.HarmonicCounterexample.Transmission.wholePeriod_value_error line 587
29. lemma OAI.HarmonicCounterexample.Transmission.wholePeriod_jet_error line 607
30. theorem OAI.HarmonicCounterexample.FiniteControl.whole_period_uniform_attainment line 675

    Source documentation

    Uniform actual WHOLE-period attainment, after factoring the entire parameter-independent diagonal leg. The error tolerance is chosen before K, Q and B, so it does not depend on the incoming history or diagonal anisotropy. Q and B have genuine Frechet derivatives.

    theorem whole_period_uniform_attainment
        (M : (MatrixProduct' (ι:=ι))ˣ) (Φ : E → MatrixProduct' (ι:=ι))
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'

31. lemma OAI.HarmonicCounterexample.FiniteControl.whole_period_exact_leg line 743

    Source documentation

    Cancellation of the factor of the ENTIRE diagonal leg gives the exact chronological target c D M. No exponentially anisotropic conjugation occurs.

    lemma whole_period_exact_leg {U V P B : MatrixProduct' (ι:=ι)} {θ : ℝ}
    …

    Mentions: OAI.HarmonicCounterexample.FiniteControl.MatrixProduct'