OAI/MathematicalPhysics/Elasticity/Compact.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElasticityCompact.flipLinear line 14

    Source documentation

    Interchanging a compact continuous-variable slot and a bounded linear slot.

    def flipLinear (q : C(A,P →L[ℝ] F)) : P →L[ℝ] C(A,F) :=
…
  2. lemma OAI.ElasticityCompact.flipLinear_apply line 25
  3. def OAI.ElasticityCompact.flipCLM line 27
  4. lemma OAI.ElasticityCompact.hasFDerivAt_compact line 42
  5. def OAI.ElasticityCompact.curryCompact line 60
  6. lemma OAI.ElasticityCompact.curryCompact_apply line 64
  7. lemma OAI.ElasticityCompact.curryCompact_continuous line 67
  8. lemma OAI.ElasticityCompact.curryCompact_hasFDerivAt line 72
  9. theorem OAI.ElasticityCompact.curryCompact_contDiff line 90

    Source documentation

    Smooth currying over a compact set. This supplies the Banach-space parameter regularity needed for the actual coefficient multipliers and linear ODE.

    theorem curryCompact_contDiff [FiniteDimensional ℝ P]
    (f : P × E → F) (hf : ContDiff ℝ (⊤ : ℕ∞) f) (j : A → E) (hj : Continuous j) :
    ContDiff ℝ (⊤ : ℕ∞) (curryCompact f hf.continuous j hj) := by
…

    Mentions: OAI.ElasticityCompact.curryCompact

  10. def OAI.ElasticityCompact.zeroExtend line 124
  11. lemma OAI.ElasticityCompact.zeroExtend_mem line 126
  12. lemma OAI.ElasticityCompact.zeroExtend_notMem line 129
  13. lemma OAI.ElasticityCompact.zeroExtend_norm line 134
  14. lemma OAI.ElasticityCompact.zeroExtend_memLp line 139
  15. lemma OAI.ElasticityCompact.zeroExtend_add line 145
  16. lemma OAI.ElasticityCompact.zeroExtend_smul line 153
  17. def OAI.ElasticityCompact.toLinfCompact line 160
  18. lemma OAI.ElasticityCompact.toLinfCompact_ae line 188
  19. theorem OAI.ElasticityCompact.exists_smooth_linf_family line 193

    Source documentation

    A joint smooth family with a fixed compact spatial support is genuinely smooth with values in L-infinity, not merely pointwise smooth.

    theorem exists_smooth_linf_family (hS : MeasurableSet S) (μ : Measure E)
    (a : P × E → ℂ) (ha : ContDiff ℝ (⊤ : ℕ∞) a)
    (hs : ∀ p x, x∉S → a (p,x)=0) :
    ∃ b : P → Lp ℂ ∞ μ, ContDiff ℝ (⊤ : ℕ∞) b ∧ ∀ p, b p =ᵐ[μ] fun x => a (p,x) := by
…