유클리드 파동방정식 국소 평활화 형식화
유클리드 파동 방정식에 대한 국소 평활화
다음은 함께 제공되는 논문과 관련된 Lean 형식화의 범위를 설명합니다.
범위
모든 차원 와 모든 \2\le p<\infty\에 대해, 이 형식화는 유클리드 반파의 노름을 그 Schwartz 초기 데이터의 노름에 상수를 곱한 값으로 상계합니다. Sobolev 차수는 모든 \varepsilon>0에 대해 이며, 에서는 도 허용됩니다. 3차원에서는 이는 임의로 작은 양의 Sobolev 손실을 갖는 임계 추정을 줍니다.
이 형식화는 또한 엄격한 범위에서 균일한 Bochner–Riesz 승수 경계, 구면 확장 추정, 그리고 Stein 제곱함수 경계를 제공합니다. Kakeya 최대 연산자는 튜브 반지름 \0<\delta\le 1\에서 모든 \varepsilon>0에 대해 손실 를 갖는 경계를 만족합니다. 의 모든 부분집합이 각 방향마다 길이 1인 선분 하나를 포함하면, 그 Hausdorff 차원은 입니다.
또한 이 전개는 튜브가 차지하는 부피에 대한 로그 하한도 증명합니다. 3차원에서는 방향이 -분리된 반지름 의 길이 1인 튜브가 적어도 개 있을 때, 중심에 무관하게 그리고 \0<\delta\le 1\에 대해 그 합집합의 부피는 최소한 입니다.
비교 링크
| 결과 | 비교 문장 |
|---|
| 유클리드 반파동 국소 평활화 | LocalSmoothing.lean |
|---|---|
| 반지름에 대해 균일한 Bochner–Riesz 승수 경계 | LocalSmoothing.lean |
| 확장 형식의 구면 제한 | LocalSmoothing.lean |
| Kakeya 최대 추정 | LocalSmoothing.lean |
| 유클리드 Kakeya 집합의 전체 하우스도르프 차원 | LocalSmoothing.lean |
| Stein 제곱함수 추정 | LocalSmoothing.lean |
출처
- 원문: https://github.com/openai/math/blob/main/lean/docs/079.md (2026-10-27 · github.com)